proposition: Lemma andE1 (T : System) (f g : Formula): SysPrf T (f /\ g)%fol -> SysPrf T f.
proof: Proof. intros H; apply nnE. apply impE with ( f /\ g)%fol. unfold andH in |- *; apply cp2. apply impI, orI1. apply Axm; right; constructor. assumption. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)