| cons F l' ⇒ FAnd F (and_of_list l')
].
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
let rec or_of_list l ≝
match l with
- [ Nil ⇒ FFalse
- | Cons F l' ⇒ FOr F (or_of_list l')
+ [ nil ⇒ FFalse
+ | cons F l' ⇒ FOr F (or_of_list l')
].
definition formula_of_sequent ≝
|4,5:
simplify in H2;
destruct H2
- | simplify in H2;
+ | simplify in H1;
destruct H1
]
|4,5:
[ decompose;
rewrite > H2; clear H2;
rewrite > H4; clear H4;
- apply (exchangeL ? a1 a2 (FAtom a));
- apply (exchangeR ? a3 a4 (FAtom a));
- apply axiom
+ apply (ExchangeL ? a1 a2 (FAtom a));
+ apply (ExchangeR ? a3 a4 (FAtom a));
+ apply Axiom
| elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
[ decompose;
rewrite > H3;
- apply (exchangeL ? a a1 FFalse);
- apply falseL
+ apply (ExchangeL ? a a1 FFalse);
+ apply FalseL
| decompose;
rewrite > H3;
- apply (exchangeR ? a a1 FTrue);
- apply trueR
+ apply (ExchangeR ? a a1 FTrue);
+ apply TrueR
]
]
qed.