proposition: Lemma eq_dec_refl : eq_dec x x = inl (id_refl x).
proof: Proof. case eq_dec; intros. apply ap. apply eq_proofs_unicity. elim e. apply id_refl. Defined.
imports: Equations.Init Equations.Type.Logic Equations.Type.Classes