proposition: Lemma ind_size0 : forall P : Te -> Prop, (forall u, (forall v, size v < size u -> P v) -> P u) -> forall u, P u.
proof: Proof. intros P h. apply intro_size. induction n; intro u; simpl; intro hs. exfalso. lia. destruct (eq_nat_dec (size u) n). subst. apply h. hyp. apply IHn. lia. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)