proposition: Lemma undef_rtc_red_is_rtc_int_red (hyp1 : forallb (@is_notvar_lhs Sig) R = true) : forall t u, red R # t u -> undefined R t = true -> int_red R # t u /\ undefined R u = true.
proof: Proof. induction 1; intro hx. ded (undef_red_is_int_red hyp1 H hx). intuition. split_all. refl. split_all. apply rt_trans with y; tauto. tauto. Qed.
imports: Coq(IndefiniteDescription ClassicalChoice ProofIrrelevance Lia) CoLoR(RelUtil ATrs LogicUtil ACalls SN InfSeq LeastNat ListUtil BoundNat NatUtil VecUtil ADP NotSN_IS ASN BoolUtil ClassicUtil)