proposition: Lemma rCompSeval_rValidComp n s phi k : Proc phi -> rValidComp phi s -> rValidComp phi (snd (rCompSeval n (k,s))).
proof: Proof. Proof with repeat (eapply validCompApp ||apply validCompClos || congruence || subst || simpl in * || intuition). intros P. unfold rCompSeval. revert s k. induction n; intros s k [? vs];(split;[auto|])... destruct s;try now inv vs;cbn... - inv vs. assert (IHn1 := IHn s1 0 ). assert (IHn2 := IHn s2 0). unfold snd,fst in *. do 2 destruct ((rCompSeval' n (_,_)))... destruct p,p0... unfold rValidComp in *. destruct b,b0... destruct (rCompBeta r r0) eqn:eq;unfold rValidComp in *. + apply IHn... eapply rCompBeta_rValidComp;eauto; unfold rValidComp in *... + idtac... - unfold rValidComp in *. inv vs. destruct s;simpl... + rewrite <- map_nth. apply H2. apply nth_In. now inv H4. + apply IHn;auto. simpl in *. split;auto. inv H4. repeat constructor... Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd