proposition: Lemma equiv_var_eq (x y: fin): var x ≡ var y -> x = y.
proof: Proof. intros; eapply equiv_unique_normal_forms in H; trivial. congruence. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)