proposition: Lemma dcong_tel_cong_tel_coerce (Δ Γ : Tel) (f : Γ) (u v : Δ) (e : u =={Δ} v) (lhs := @dcong_tel Δ (fun _ => Γ) (fun _ => f) u v e) (rhs := @cong_tel Δ Γ (fun _ => f) u v e) : Type.
proof: Proof. simpl in *. pose (subst (fun _ => Γ) u v e). unfold eq_expl in *. unfold dcong_tel. unfold Telescopes.dcong_tel_obligation_1. unfold eq_rect_r. unfold J_refl. simpl. set(lhs := cong_tel _ _ _ _). simpl in lhs. set(rhs1 := dcong_tel _ _ _ _). set(rhs2 := dcong_tel _ _ _ _). simpl in *. unfold dcong_tel. apply axiom. refine (equiv_id _). Defined.
imports: Equations DepElimDec EqDecInstances Utf8