proposition: Lemma undef_red_is_int_red : forall (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. intros hyp1 t u tu ht. unfold undefined in ht. destruct t. discr. redtac. destruct l. rewrite forallb_forall in hyp1. ded (hyp1 _ lr). discr. ded (fun_eq_fill xl). decomp H. subst. simpl in xl. Funeqtac. rewrite (lhs_fun_defined lr) in ht. discr. split. rewrite xl, yr. ex (Fun f0 t0) r c s. split_all. congruence. subst. 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)