proposition: Lemma eq_refl (t:Term L): Prf L nil (t = t)%fol.
proof: Proof. assert (H: Prf L nil (allH 0, v#0 = v#0)%fol). { apply GEN. - cbn; auto. - apply EQ1. } change (nil:(list (Formula L))) with (nil++nil: list(Formula L)). eapply MP. 2: apply H. apply (FA1 _ (v#0 = v#0)%fol 0 t). Defined.
imports: Coq(Arith Lists.List) hydras.Ackermann(fol folProp folProof Languages folLogic folLogic2 folLogic3 subAll Deduction primRec)