proposition: Lemma subterm_eq_proj_sub : forall s t, subterm_eq (proj (sub s t)) (sub s (proj t)).
proof: Proof. intros. case t. simpl. intros. apply subterm_eq_proj. intros. rewrite proj_sub_fun. refl. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)