proposition: Lemma term_eqb_spec : forall x y1 : term, reflect (x = y1) (term_eqb x y1).
proof: Proof. Proof with try (constructor;congruence). induction x;cbn; destruct y1... - destruct (eqb_spec n n0)... - destruct (IHx1 y1_1)... destruct (IHx2 y1_2)... - destruct (IHx y1)... Qed.
imports: Nat Undecidability.L(Tactics.LTactics Functions.EqBool)