proposition: Lemma inj_extend_tel_equiv@{i} (Γ : Tel@{i}) (u v : Γ) (Δ : Tel@{i}) (a b : Γ → Δ) (eqΔ:=λ ρ : Γ, a ρ =={Δ} b ρ) (r : eqΔ u) (s : eqΔ v) : inj_extend_tel Γ eqΔ u r =={extend_tele Γ eqΔ} inj_extend_tel Γ eqΔ v s <~> extend_tele (u =={Γ} v) (λ x : u =={Γ} v, square_tel r s (cong_tel a x) (cong_tel b x)).
proof: Proof. induction Γ. Transparent telescope eq. - simpl extend_tele. simpl inj_extend_tel. refine (equiv_tele_r _). intros x. unfold square_tel. simpl in x. revert v x s. refine (Top.J@{i i} _ _). intros s. simpl. unfold square_tel. unfold cong_tel. simpl. subst eqΔ. simpl in *. refine (equiv_sym _). apply subst_subst. - simpl. refine (equiv_tele_r _). intros. destruct v. simpl in *. subst eqΔ. simpl in *. revert pr1 x pr2 s. refine (Top.J@{i i} _ _). simpl. intros. specialize (X u.1 u.2 pr2). specialize (X (fun ρ => a &(u.1 & ρ))). simpl in X. specialize (X (fun ρ => b &(u.1 & ρ))). simpl in X. destruct u. simpl in *. specialize (X r s). apply X. Defined.
imports: Equations Utf8 DepElimDec EqDecInstances