proposition: Lemma supterm_red : supterm @ red R << red R @ supterm.
proof: Proof. intros x z [y [xSuby yRz]]. inversion xSuby as [C [notHoleC fillCy]]. inversion yRz as [l [r [Cred [s [rule [yfillCredl zfillCredr]]]]]]. exists (fill C z). split. exists l. exists r. exists (comp C Cred). exists s. split. hyp. split. rewrite <- fill_fill, <- yfillCredl. hyp. rewrite <- fill_fill, <- zfillCredr. refl. exists C. split. hyp. refl. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)