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