constructor 1;
[ apply A
| intros;
- alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
apply True
| intro;
constructor 1
constructor 1;
[ apply A
| intros;
- alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
apply True
| intro;
constructor 1
|
|
|
-*)
\ No newline at end of file
+*)