proposition: Lemma rc_supterm : supterm_eq == supterm%.
proof: Proof. rewrite rel_eq. intros t u. split; intro h. destruct h. destruct x. left. auto. right. exists (Cont e t0 x t1). intuition. discr. destruct h. exists Hole. auto. apply subterm_strict. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)