proposition: Lemma ind_size1 : forall P : Te -> Prop, (forall x, P (Var x)) -> (forall f, P (Fun f)) -> (forall u v, P u -> P v -> P (App u v)) -> (forall x u, (forall u', size u' <= size u -> P u') -> P (Lam x u)) -> forall u, P u.
proof: Proof. intros P hv hf ha hl. apply ind_size0. intros [x|f|u v|x u] h. apply hv. apply hf. apply ha; apply h; simpl; max. apply hl. intros u' h'. apply h. simpl. lia. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)