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