proposition: Lemma freeVarInterpFormula (v1 v2 : nat -> U M) (g : Formula L): (forall x : nat, List.In x (freeVarF g) -> v1 x = v2 x) -> interpFormula v1 g -> interpFormula v2 g.
proof: Proof. revert v1 v2. induction g as [t t0| r t| g1 Hrecg1 g0 Hrecg0| g Hrecg| n g Hrecg]; simpl in |- *; intros v1 v2 H. - repeat rewrite (freeVarInterpTerm v1 v2). + auto. + intros x H0; apply H. simpl; auto with datatypes. + intros x H0; apply H. simpl; auto with datatypes. - intros H0; apply (freeVarInterpRel v1 v2). + apply H. + apply H0. - assert (H0: interpFormula v2 g1 -> interpFormula v1 g1). { apply Hrecg1. intros x H0; symmetry; apply H. simpl; auto with datatypes. } assert (H1: interpFormula v1 g0 -> interpFormula v2 g0). { apply Hrecg0. intros x H1; apply H; simpl; auto with datatypes. } tauto. - intros H0 H1; apply H0. apply Hrecg with v2. intros x H2; symmetry; auto. assumption. - intros H0 x; apply Hrecg with (updateValue v1 n x). + intros x0 H1; unfold updateValue; induction (eq_nat_dec n x0). * reflexivity. * apply H. apply in_in_remove; auto. + auto. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)