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