proposition: Lemma cong_tel_proj@{i} (Δ : Tel@{i}) (A : Type@{i}) (Γ : A -> Tel@{i}) (f : Δ → ext A Γ) (u v : Δ) (e : u =={Δ} v) : (cong_tel f e).1 = cong_tel (Γ:=inj A) (fun x => (f x).1) e.
proof: Proof. induction Δ. + revert v e. refine (J@{i i i} _ _ _). simpl. unfold cong_tel. simpl. reflexivity. + revert v e. refine (J@{i i i} _ _ _). simpl. specialize (H u.1 (fun t => f &(u.1 & t)) u.2 u.2 (refl _)). unfold cong_tel at 1. simpl. unfold cong_tel in H. rewrite H. reflexivity. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances