proposition: Lemma solution_left_dep : forall {A} (t : A) {B : forall (x : A), (x = t -> Type)}, B t eq_refl -> (forall x (Heq : x = t), B x Heq).
proof: Proof. intros A t B H x eq. apply eq_symmetry_dep. clear eq. intros. destruct eq. exact H. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.CoreTactics Equations.Signature Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec