proposition: Lemma openClosed (T : System) (f : Formula): SysPrf T (close L f) -> SysPrf T f.
proof: Proof. unfold close; generalize (List.nodup Peano_dec.eq_nat_dec (freeVarF f)); intros l H; induction l as [| a l Hrecl]. - apply H. - simpl in H; apply Hrecl; eapply forallSimp; apply H. Qed.
imports: Coq(Ensembles List) hydras.Ackermann(ListExt folProof folProp Deduction)