proposition: Lemma cong_tel_nondep@{i} {Δ Γ : Tel@{i}} (T : Γ) (u v : Δ) (e : u =={Δ} v) : cong_tel (fun _ => T) e == refl T.
proof: Proof. revert v e. refine (J _ _ _). unfold cong_tel. rewrite J_refl. apply refl. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances