proposition: Lemma supterm_R_mon_commut : supterm @ R << R @ supterm.
proof: Proof. intros t v [u [tu uv]]; revert t u tu v uv; induction 1. intros u' uu'. exists (App u' v). split. mon. apply st_app_l. intros v' vv'. exists (App u v'). split. mon. apply st_app_r. intros u' uu'. exists (Lam x u'). split. mon. apply st_lam. Qed.
imports: Coq(FSets Structures.OrderedType) CoLoR(LogicUtil BoolUtil VecUtil FSetUtil NatUtil RelUtil SN SetUtil)