fact: Definition solution_left {A} {B : A -> Type} (t : A) (p : B t) (x : A) (e : x = t) : B x := eq_sym e # p.
imports: Coq.Program.Tactics Equations.Init Equations.CoreTactics Equations.Signature Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec