(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
(* Basic_1: removed theorems 11:
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
(* Basic_1: removed theorems 11:
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O