proposition: Lemma reduceCloseList (l : list nat) (f1 f2 : Formula) (T : System): (forall v : nat, In v l -> ~ In_freeVarSys _ v T) -> SysPrf T (iffH f1 f2) -> SysPrf T (iffH (closeList L l f1) (closeList L l f2)).
proof: Proof. revert T f1 f2; induction l as [| a l Hrecl]; simpl in |- *; intros. - apply H0. - apply reduceForall. + apply H; now left. + apply Hrecl; auto. Qed.
imports: Coq(Ensembles Lists.List Peano_dec) hydras.Ackermann(ListExt folProof folLogic folProp)