proposition: Lemma equiv_tele_r {A} {B B' : A -> Type} (e : forall x : A, Equiv (B x) (B' x)) : tele (x : A) in B x <~> tele (x : A) in (B' x).
proof: Proof. simpl. unshelve refine {| equiv a := &(a.1 & e a.1 a.2) |}. unshelve refine {| equiv_inv a := &(a.1 & inv_equiv (e a.1) a.2) |}. red; intros. simpl. destruct x. simpl. apply Top.cong. apply eisretr. red; intros. simpl. destruct x. simpl. apply Top.cong. apply eissect. intros [x bx]. simpl. rewrite eisadj. simpl. destruct (eissect (e x) bx). simpl. reflexivity. Defined.
imports: Equations DepElimDec EqDecInstances Utf8