proposition: Lemma eqRefl (T : fol.System L) (a : fol.Term L): SysPrf T (a = a)%fol.
proof: Proof. replace (a = a)%fol with (substF (v#0 = v#0)%fol 0 a). apply (forallE L). - apply sysExtend with (Empty_set (fol.Formula L)). + intros f H; destruct H. + apply forallI. * apply (notInFreeVarSys L). * exists (nil (A:=fol.Formula L)). exists (EQ1 L); contradiction. - rewrite (subFormulaEqual L); reflexivity. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)