proposition: Lemma equiv_cong_subst_dep {A} {B : A -> Type} (P : forall x : A, B x -> Type) (f : forall x : A, B x) (s t : A) (e : s = t) (u : P s (f s)) (v : P t (f t)) : u =_{(fun x => P x (f x)); e} v <~> (Top.J (fun y e => P y (rew e in (f s))) u _ e =_{(fun x => P _ x); Top.congd f e} v).
proof: Proof. unfold Top.subst. destruct e. simpl. apply equiv_id. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances