proposition: Lemma equiv_tele_l {A} {A'} {B : A' -> Type} (e : Equiv A A') : tele (x : A) in B (equiv e x) <~> tele (x : A') in B x.
proof: Proof. simpl. unshelve refine {| equiv a := &(e a.1 & _) |}. exact a.2. unshelve refine {| equiv_inv a := &(e ^-1 a.1 & _) |}. destruct a. simpl. rewrite eisretr. exact pr2. red; intros. simpl. destruct x. simpl. pose (eisretr e pr1). apply path_sigma_uncurried. simpl. exists e0. simpl. unfold eq_rect_r. clearbody e0. apply axiom. apply axiom. apply axiom. Defined.
imports: Equations DepElimDec EqDecInstances Utf8