proposition: Lemma REPEAT_SinvT : forall (P : Signal _ Act del -> Process -> Stream A -> Prop) (w : Signal _ Act del) (q : Process) (s : Stream A), P (Clear _ Act del (hd s)) (REPEAT (tl s)) s -> SafeProcTrans Channel Act del (REPEAT s) (Transmit _ Act del w) q -> P w q s.
proof: Proof. intros P w q s H. rewrite unfold_REPEAT. intro H0. simple inversion H0. rewrite <- H3. injection H2 as <-. rewrite (inj_Tmess del v (hd s) p (REPEAT (tl s)) c2 del f (fun _ : A => REPEAT s)) . 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