proposition: Lemma reorder_tele@{i +} (Δ : t@{i}) (Γ : telescope Δ -> t@{i}) : telescope (extend_tele Δ Γ) <~> tele (x : telescope Δ) in Γ x.
proof: Proof. unshelve econstructor. - induction Δ; simpl extend_tele in *; simpl; intros. trivial. simpl in Γ. specialize (X X0.1 _ X0.2). refine &(&(X0.1 & X.1)&X.2). - unshelve econstructor. + induction Δ; simpl extend_tele in *; intros; simpl in *; trivial. specialize (X X0.1.1). exists X0.1.1. apply X. exact &(X0.1.2 & X0.2). + red. intro. induction Δ; simpl. destruct x. constructor. destruct x. simpl. rewrite H. reflexivity. + red. intro. induction Δ; simpl. destruct x. constructor. destruct x. simpl. rewrite H. reflexivity. + apply axiom_triangle. Defined.
imports: Equations Utf8 DepElimDec