proposition: Lemma tforall_forall {TT : tele} (Ψ : TT → Prop) : tforall Ψ ↔ (∀ x, Ψ x).
proof: Proof. symmetry. unfold tforall. induction TT as [|X ft IH]. - simpl. split. + done. + intros ? p. rewrite (tele_arg_O_inv p). done. - simpl. split; intros Hx a. + rewrite <-IH. done. + destruct (tele_arg_S_inv a) as [x [pf ->]]. revert pf. setoid_rewrite IH. done. Qed.
imports: stdpp(base tactics) stdpp(options)