proposition: Lemma exist_eq {A} (P : A -> Prop) (x y : A) (p : P x) (q : P y) : { e : x = y & eq_rect _ P p _ e = q } -> exist _ x p = exist _ y q.
proof: Proof. intros [He Hp]. destruct He. simpl in Hp. destruct Hp. reflexivity. Defined.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia