proposition: Lemma intro_size : forall P : Te -> Prop, (forall n u, size u < n -> P u) -> forall u, P u.
proof: Proof. intros P h u. eapply h with (n:=S(size u)). lia. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)