proposition: Lemma tele_arg_inv {TT : tele} (a : tele_arg TT) : match TT as TT return tele_arg TT → Prop with | TeleO => λ a, a = TargO | TeleS f => λ a, ∃ x a', a = TargS x a' end a.
proof: Proof. destruct TT; destruct a; eauto. Qed.
imports: stdpp(base tactics) stdpp(options)