proposition: Lemma eq_symmetry_dep {A} {t : A} {B : forall (x : A), x = t -> Type} : (forall (x : A) (eq : t = x), B x (inverse eq)) -> (forall (x : A) (eq : x = t), B x eq).
proof: Proof. intros. rewrite <- eq_sym_invol. generalize (inverse eq). apply X. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.Signature Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec