(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
include "nat/plus.ma".
include "nat/compare.ma".
include "list/sort.ma".
[1,2:
simplify in H;
destruct H
- | generalize in match H; clear H;
- elim f2;
+ | elim f2 in H ⊢ %;
[1,2:
simplify in H;
destruct H
intros;
lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
simplify in Hletin;
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
[ intros;
simplify in H2;
- generalize in match H2; clear H2;
- generalize in match H1; clear H1;
- generalize in match H; clear H;
- elim l2 0;
+ elim l2 in H2 H1 H ⊢ % 0;
[ intros;
simplify in H2;
destruct H2
| assumption
| lapply (H2 n1); clear H2;
simplify in Hletin;
- generalize in match Hletin; clear Hletin;
- elim (eqb n1 n);
+ elim (eqb n1 n) in Hletin ⊢ %;
[ simplify in H2;
rewrite > H2;
autobatch
rewrite > eqb_n_n in H3;
simplify in H3;
(*
- generalize in match H3;
- generalize in match H1; clear H1;
- generalize in match H; clear H;
- elim l 0;
+ elim l in H3 H1 H ⊢ % 0;
[ elim l2 0;
[ intros;
simplify in H2;
]
[ autobatch
- | generalize in match H4; clear H4;
- generalize in match H2; clear H2;
- elim t1;
+ | elim t1 in H4 H2 ⊢ %;
[
|
|