proposition: Lemma andI (T : System) (f g : Formula): SysPrf T f -> SysPrf T g -> SysPrf T (f /\ g)%fol.
proof: Proof. intros H H0; unfold andH; apply orE with (~ (~f \/ ~g))%fol (~ f \/ ~g)%fol. - apply noMiddle. - apply impI, Axm; right; constructor. - apply impI; apply orE with (~ f)%fol (~ g)%fol. + apply Axm; right; constructor. + apply cp2; apply impI. repeat apply sysWeaken; assumption. + apply cp2; apply impI. repeat apply sysWeaken; assumption. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)