proposition: Lemma eq_sound : forall x y, eq x y = true -> x = y.
proof: Proof. intros [b1 u1][b2 u2]; unfold eq; case (ext_eq b1 b2); case (ext_eq u1 u2); try (intros; discriminate). intros; subst; auto. Qed.
imports: ZArith List Lia