proposition: Lemma term_beq_sound x y : term_beq x y = true → x = y.
proof: Proof. induction x, y; simpl; intros; intuition. - apply Pos.eqb_eq in H; subst; reflexivity. - apply N.eqb_eq in H; subst; reflexivity. Defined.
imports: Coq.NArith.NArith Coq.FSets.FMaps Coq.micromega.Lia Category.Lib Category.Lib.FMapExt