proposition: Lemma dcong_tel_cong_tel' (Δ Γ : Tel) (f : Γ) (u v : Δ) (e : u =={Δ} v) : f =={fun _ => Γ; e} f = (f == f).
proof: Proof. revert v e. refine (J _ _ _). unfold subst. rewrite J_refl. reflexivity. Defined.
imports: Equations DepElimDec EqDecInstances Utf8