proposition: Lemma WF_hd_red_Mod_int : forall (hyp1 : forallb (@is_notvar_lhs Sig) R = true) (hyp2 : forallb (undefined_rhs R) D = true), WF (hd_red_Mod (int_red R #) D) -> WF (hd_red_mod R D).
proof: Proof. intros hyp1 hyp2. intro wf. unfold hd_red_mod. apply WF_mod_rev2. apply WF_mod_rev in wf. intro t. gen (wf t). induction 1. apply SN_intro. intros z [y [xy yz]]. apply H0. exists y. split_all. assert (hy : undefined R y = true). redtac. rewrite forallb_forall in hyp2. gen (hyp2 _ lr). unfold undefined_rhs. simpl. unfold undefined. subst. destruct r. discr. simpl. auto. destruct (undef_rtc_red_is_rtc_int_red hyp1 yz hy). hyp. 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)