If there is a way to define a "local" Ltac expresion which I can use to proof a lemma but not visible outside?
Lemma Foo ...
Proof.
Ltac ll := ...
destrict t.
- reflexivity.
- ll.
- ll.
Qed.
(* ll should not be visible here *)
You can use a section:
Section Foo.
Ltac solve := exact I.
Lemma Foo : True.
Proof.
solve.
Qed.
End Foo.