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