| 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: