proposition: Lemma texist_exist {TT : tele} (Ψ : TT → Prop) : texist Ψ ↔ ex Ψ.
proof: Proof. symmetry. induction TT as [|X ft IH]. - simpl. split. + intros [p Hp]. rewrite (tele_arg_O_inv p) in Hp. done. + intros. by exists TargO. - simpl. split; intros [p Hp]; revert Hp. + destruct (tele_arg_S_inv p) as [x [pf ->]]. intros ?. exists x. rewrite <-(IH x (λ a, Ψ (TargS x a))). eauto. + rewrite <-(IH p (λ a, Ψ (TargS p a))). intros [??]. eauto. Qed.
imports: stdpp(base tactics) stdpp(options)