proposition: Lemma equiv_cong_subst_tel {Δ Γ : Tel} (P : Γ -> Tel) (f : Δ -> Γ) (s t : Δ) (e : s =={Δ} t) (u : P (f s)) : subst P (cong_tel f e) u = subst (fun x => P (f x)) e u.
proof: Proof. unfold subst. revert t e. refine (J _ _ _). intros. rewrite J_refl. unfold cong_tel. simpl. rewrite !J_refl. reflexivity. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances