proposition: Lemma eqSym (T : fol.System L) (a b : fol.Term L): SysPrf T (a = b)%fol -> SysPrf T (b = a)%fol.
proof: Proof. intros H;apply (impE L) with (equal a b); [ | easy]. set (m := fun x : nat => match x with | O => a | S _ => b end) in *. apply (impE L) with (subAllFormula L (v#0 = v#1 -> v#1 = v#0)%fol (fun x : nat => match le_lt_dec 2 x with | left _ => var x | right _ => m x end)). + simpl; destruct (le_lt_dec 2 0) as [l | l]. * lia. * destruct (le_lt_dec 2 1) as [l0 | l0]. -- lia. -- apply (impRefl L). + apply (subAllCloseFrom L). apply sysExtend with (Empty_set (fol.Formula L)). * intros x H0; destruct H0. * simpl; apply forallI. -- apply (notInFreeVarSys L). -- apply forallI. ++ apply (notInFreeVarSys L). ++ exists (nil (A:=fol.Formula L)). exists (EQ2 L); contradiction. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)