proposition: Lemma OUT_SinvT : forall (P : Signal _ Act del -> Process -> bool -> A -> Prop) (w : Signal _ Act del) (q : Process) (b : bool) (a : A), P (Clear _ Act del a) (ACK b) b a -> SafeProcTrans Channel Act del (OUT b a) (Transmit _ Act del w) q -> P w q b a.
proof: Proof. intros P w q b a H. rewrite unfold_OUT. intros H0. simple inversion H0. rewrite <- H3. injection H2 as <-. rewrite (inj_Tmess del v a p (ACK b) c2 lnk1 f (fun _ : bool * A => OUT b a)). injection H1 as ? ->. assumption. assumption. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. discriminate H3. Defined.
imports: ABP.ABP.BISIMULATION.Hypotheses