proposition: Lemma rCompBeta_sound phi (s t u: rComp) : Proc phi -> rCompBeta s t = Some u -> denoteComp phi (s t) >[(1)] denoteComp phi u.
proof: Proof. Proof with simpl in *;try congruence;auto. intros pp eq. destruct s... destruct s... destruct t... destruct s0; inv eq... - constructor. apply pp. - constructor. eexists. reflexivity. Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd