proposition: Lemma eq_sym_dep {A} (x y : A) (P : x = y -> Type) (G : forall e : y = x, P (eq_sym e)) : forall e : x = y, P e.
proof: Proof. intros. destruct e. apply (G eq_refl). Defined.
imports: Equations Utf8 DepElimDec EqDecInstances