proposition: Lemma rtc_red_one_flat_cont_intro : forall t u, red R # t u -> red (flat_rules R) # (fill one_flat_cont t) (fill one_flat_cont u).
proof: Proof. induction 1. apply rt_step. apply red_one_flat_cont_intro. hyp. apply rt_refl. apply rt_trans with (fill one_flat_cont y); hyp. Qed.
imports: CoLoR(ATrs NatUtil LogicUtil ListUtil SN EqUtil VecUtil RelUtil BoundNat)