proposition: Lemma expressibleAlternate : forall (n : nat) (R : naryRel n) (A B : Formula), SysPrf T (iffH A B) -> ExpressibleHelp n R A -> ExpressibleHelp n R B.
proof: Proof. induction n as [| n Hrecn]; intros. - induction R. + simpl in H0 |- *. apply impE with A. * apply iffE1, H. * apply H0. + simpl in H0 |- *. apply impE with (~ A)%fol. * apply cp2. now apply iffE2. * apply H0. - simpl in H0 |- *. intros a; apply (Hrecn (R a)) with (substF A (S n) (natToTerm a)). + rewrite <- (subFormulaIff LNN). apply forallE. apply forallI. * now apply closedT. * auto. + apply H0. Qed.
imports: Coq(Arith List) hydras.Ackermann(ListExt folProp subProp extEqualNat Languages LNN NewNotations)