proposition: Lemma solution_right_dep@{i j|} : forall {A : Type@{i}} (t : A) {B : forall (x : A), (t = x -> Type@{j})}, B t 1 -> (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.Signature Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec