proposition: Lemma tele_arg_ind (P : ∀ TT, tele_arg TT → Prop) : P TeleO TargO → (∀ T (b : T → tele) x xs, P (b x) xs → P (TeleS b) (TargS x xs)) → ∀ TT (xs : tele_arg TT), P TT xs.
proof: Proof. intros H0 HS TT. induction TT as [|T b IH]; simpl. - by intros []. - intros [x xs]. by apply HS. Qed.
imports: stdpp(base tactics) stdpp(options)