(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                                                          *)
(*      Coq V5.8                                                            *)
(*                                                                          *)
(*                                                                          *)
(*      Alternating Bit Protocol                                            *)
(*                                                                          *)
(*      Jan Friso Groote                                                    *)
(*      Utrecht University                                                  *)
(*                                                                          *)
(*      November 1992                                                       *)
(*                                                                          *)
(* From bezem@phil.ruu.nl Fri Apr  2 13:14:31 1993                          *)
(*                                                                          *)
(****************************************************************************)
(*                                abp_proc.v                                *)
(****************************************************************************)

Require Import abp_base.
Require Import abp_defs.
Require Import abp_lem1.
Require Import abp_lem2.
Require Import abp_lem25.
Require Import abp_lem3.

Require Import abp_lem1.

(* Now we define a number of simplified processes *)

Parameter X' Y' : proc.
Parameter X1' X2' Y1' Y2' : D -> proc.


Axiom
  Lin2' :
    forall d : D,
    alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d))))
      (seq (ia one int i) (seq (ia one int i) (X1' d))) = 
    X1' d.


Axiom
  Lin3' :
    forall d : D,
    alt (seq (ia one int i) (seq (ia one int i) (X2' d)))
      (seq (ia one int i) (hide I' Y)) = X2' d.



Axiom
  Lin5' :
    forall d : D,
    alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))
      (seq (ia one int i) (seq (ia one int i) (Y1' d))) = 
    Y1' d.

Axiom
  Lin6' :
    forall d : D,
    alt (seq (ia one int i) (seq (ia one int i) (Y2' d)))
      (seq (ia one int i) (hide I' X)) = Y2' d.


Goal forall d : D, seq (ia one tau i) (X1' d) = hide I' (X1 d).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
apply
 (RSP D (fun d : D => seq (ia one tau i) (X1' d))
    (fun d : D => hide I' (X1 d))
    (fun (X : D -> proc) (d : D) =>
     seq (ia one tau i)
       (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d))))
          (seq (ia one int i) (seq (ia one int i) (X d)))))).
(* Goal: forall (p : forall _ : D, proc) (d : D), GRD (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (p d))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (Y2' d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
auto.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
(* Goal: @eq proc (seq (ia one tau i) (X1' d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (X2 d0)))) (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (X1' d0)))))) *)
(* Goal: forall d : D, @eq proc (hide I' (X1 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))) (seq (ia one int i) (seq (ia one int i) (hide I' (X1 d)))))) *)
pattern (X1' d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (X1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))))) (X1' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (X2 d))))) *)
elim Lin2'.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.

(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
(* Goal: @eq proc (hide I' (X1 d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (X2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (X1 d0)))))) *)
pattern (X1 d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (hide I' p) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (X2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (X1 d0))))))) (X1 d0) *)
elim Lem12.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (alt (ia one int i) (ia one int i)) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim A3.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
repeat elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (seq (ia one int i) (ia one tau i)) (hide I' (Y1 d0)))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0)))))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
elim T1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c5 I' *)
exact Inc5I.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
exact Ins4I.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc2I.

Save LemLin2.

Goal forall d : D, seq (ia one tau i) (X2' d) = hide I' (X2 d).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
apply
 (RSP D (fun d : D => seq (ia one tau i) (X2' d))
    (fun d : D => hide I' (X2 d))
    (fun (X : D -> proc) (d : D) =>
     seq (ia one tau i)
       (alt (seq (ia one int i) (seq (ia one int i) (X d)))
          (seq (ia one int i) (hide I' Y))))).
(* Goal: forall (p : forall _ : D, proc) (d : D), GRD (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (p d))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (Y2' d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
auto.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (seq (ia one tau i) (X2' d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (X2' d0)))) (seq (ia one int i) (hide I' Y)))) *)
(* Goal: forall d : D, @eq proc (hide I' (X2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (X2 d)))) (seq (ia one int i) (hide I' Y)))) *)
pattern (X2' d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (X2' d))) (seq (ia one int i) (hide I' Y)))) (X2' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' Y)))) (seq (ia one tau i) (hide I'' (hide I' Y))) *)
elim Lin3'.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (hide I' (X2 d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (X2 d0)))) (seq (ia one int i) (hide I' Y)))) *)
pattern (X2 d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (hide I' p) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (X2 d0)))) (seq (ia one int i) (hide I' Y))))) (X2 d0) *)
elim Lem31.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.

(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.

(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
repeat elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (seq (ia one int i) (ia one tau i)) (hide I' (Y1 d0)))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0)))))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
repeat elim T1.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (alt (ia one int i) (ia one int i)) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim A3.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc2I.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c5 I' *)
exact Inc5I.
Save LemLin3.

Goal forall d : D, seq (ia one tau i) (Y1' d) = hide I' (Y1 d).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
apply
 (RSP D (fun d : D => seq (ia one tau i) (Y1' d))
    (fun d : D => hide I' (Y1 d))
    (fun (Y : D -> proc) (d : D) =>
     seq (ia one tau i)
       (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))
          (seq (ia one int i) (seq (ia one int i) (Y d)))))).
(* Goal: forall (p : forall _ : D, proc) (d : D), GRD (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (p d))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (Y2' d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
auto.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
(* Goal: @eq proc (seq (ia one tau i) (Y1' d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y1' d0)))))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y1 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d)))))) *)
pattern (Y1' d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (Y1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (Y1' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
elim Lin5'.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
(* Goal: @eq proc (hide I' (Y1 d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0)))))) *)
pattern (Y1 d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (hide I' p) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0))))))) (Y1 d0) *)
elim Lem22.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (alt (ia one int i) (ia one int i)) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim A3.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
repeat elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (seq (ia one int i) (ia one tau i)) (hide I' (Y1 d0)))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0)))))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
elim T1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c5 I' *)
exact Inc5I.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
exact Ins4I.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc2I.
Save LemLin5.

Goal forall d : D, seq (ia one tau i) (Y2' d) = hide I' (Y2 d).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
apply
 (RSP D (fun d : D => seq (ia one tau i) (Y2' d))
    (fun d : D => hide I' (Y2 d))
    (fun (Y : D -> proc) (d : D) =>
     seq (ia one tau i)
       (alt (seq (ia one int i) (seq (ia one int i) (Y d)))
          (seq (ia one int i) (hide I' X))))).
(* Goal: forall (p : forall _ : D, proc) (d : D), GRD (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (p d))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (Y2' d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
auto.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (seq (ia one tau i) (Y2' d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
pattern (Y2' d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (Y2' d))) (seq (ia one int i) (hide I' X)))) (Y2' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim Lin6'.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (hide I' (Y2 d0)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
pattern (Y2 d0) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (hide I' p) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X))))) (Y2 d0) *)
elim Lem41.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.

(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one tau i) (seq (ia one tau i) (seq (hide I' (alt (seq (ia one int i) (ia Frame c3 lce)) (seq (ia one int i) (ia Frame c3 (Tuple e1 d0))))) (hide I' (Y2 d0)))))) (hide I' (seq (ia one int i) (seq (ia frame c6 (tuple e1)) X))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim TI4.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.

(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
repeat elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (seq (ia one int i) (ia one tau i)) (hide I' (Y1 d0)))))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia D s4 d0) (hide I' (Y2 d0)))) (seq (ia one int i) (seq (ia one int i) (hide I' (Y1 d0)))))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: not (In_ehlist s4 I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
repeat elim T1.
(* Goal: @eq proc (seq (ia one tau i) (alt (seq (ia one int i) (seq (alt (ia one int i) (ia one int i)) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d0)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
elim A3.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c3 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc3I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c2 I' *)
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc2I.
(* Goal: In_ehlist c6 I' *)
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact Inc6I.
(* Goal: not (In_ehlist int I') *)
(* Goal: In_ehlist c5 I' *)
exact InintI.
(* Goal: In_ehlist c5 I' *)
exact Inc5I.
Save LemLin6.


Goal
forall d : D,
seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (X2 d)))) =
seq (ia one tau i) (hide I'' (X1' d)).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
apply sym_equal.
elimtype
 (seq (ia one tau i)
    (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d))))) =
  seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (X2 d))))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (Y2' d))) (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
apply (KFAR2 one i int).
(* Goal: In_ehlist int I'' *)
exact InintI''.
(* Goal: @eq proc (X1' d) (alt (seq (ia one int i) (seq (ia one int i) (X1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d))))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (X2 d))))) *)
pattern (X1' d) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (X1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))))) (X1' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (X2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (X2 d))))) *)
elim Lin2'.
(* Goal: @eq proc (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))) (seq (ia one int i) (seq (ia one int i) (Y1' d)))) (alt (seq (ia one int i) (seq (ia one int i) (Y1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
elim A1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: not (In_ehlist s4 I'') *)
(* Goal: In_ehlist int I'' *)
exact Ins4I''.
(* Goal: In_ehlist int I'' *)
exact InintI''.
Save KFlin2.

Goal
forall d : D,
seq (ia one tau i) (hide I'' (hide I' Y)) =
seq (ia one tau i) (hide I'' (X2' d)).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
apply sym_equal.
elimtype
 (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' Y))) =
  seq (ia one tau i) (hide I'' (hide I' Y))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (Y2' d))) (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
apply (KFAR2 one i int).
(* Goal: In_ehlist int I'' *)
exact InintI''.
(* Goal: @eq proc (X2' d) (alt (seq (ia one int i) (seq (ia one int i) (X2' d))) (seq (ia one int i) (hide I' Y))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' Y)))) (seq (ia one tau i) (hide I'' (hide I' Y))) *)
pattern (X2' d) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (X2' d))) (seq (ia one int i) (hide I' Y)))) (X2' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' Y)))) (seq (ia one tau i) (hide I'' (hide I' Y))) *)
elim Lin3'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: In_ehlist int I'' *)
exact InintI''.
Save KFlin3.

Goal
forall d : D,
seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d)))) =
seq (ia one tau i) (hide I'' (Y1' d)).
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
apply sym_equal.
elimtype
 (seq (ia one tau i)
    (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))) =
  seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (Y2' d))) (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
apply (KFAR2 one i int).
(* Goal: In_ehlist int I'' *)
exact InintI''.
(* Goal: @eq proc (Y1' d) (alt (seq (ia one int i) (seq (ia one int i) (Y1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
pattern (Y1' d) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (Y1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (Y1' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
elim Lin5'.
(* Goal: @eq proc (alt (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))) (seq (ia one int i) (seq (ia one int i) (Y1' d)))) (alt (seq (ia one int i) (seq (ia one int i) (Y1' d))) (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d))))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (seq (ia D s4 d) (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
elim A1.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5. 
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1. 
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: not (In_ehlist s4 I'') *)
(* Goal: In_ehlist int I'' *)
exact Ins4I''. 
(* Goal: In_ehlist int I'' *)
exact InintI''. 
Save KFlin5. 

Goal
forall d : D,
seq (ia one tau i) (hide I'' (hide I' X)) =
seq (ia one tau i) (hide I'' (Y2' d)). 
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
intros. 
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
apply sym_equal. 
elimtype
 (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X))) =
  seq (ia one tau i) (hide I'' (hide I' X))). 
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (Y2' d))) (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
apply (KFAR2 one i int). 
(* Goal: In_ehlist int I'' *)
exact InintI''. 
(* Goal: @eq proc (Y2' d) (alt (seq (ia one int i) (seq (ia one int i) (Y2' d))) (seq (ia one int i) (hide I' X))) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
pattern (Y2' d) at 1 in |- *. 
(* Goal: (fun p : proc => @eq proc p (alt (seq (ia one int i) (seq (ia one int i) (Y2' d))) (seq (ia one int i) (hide I' X)))) (Y2' d) *)
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim Lin6'.  

(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal. 
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5. 
(* Goal: @eq proc (seq (ia one tau i) (seq (hide I'' (ia one int i)) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'. 
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal. 
(* Goal: In_ehlist int I'' *)
exact InintI''.
Save KFlin6.

Parameter B : proc.
Axiom Specificat : D + (fun d : D => seq (ia D r1 d) (seq (ia D s4 d) B)) = B.

Goal B = hide I'' (hide I' ABP).

apply
 (RSP one (fun d : one => B) (fun d : one => hide I'' (hide I' X))
    (fun (Z : one -> proc) (d' : one) =>
     D +
     (fun d : D =>
      seq (ia D r1 d)
        (seq (ia D s4 d)
           (D + (fun d : D => seq (ia D r1 d) (seq (ia D s4 d) (Z d')))))))).
(* Goal: forall (p : forall _ : D, proc) (d : D), GRD (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (p d))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (Y2' d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (seq (ia one tau i) (Y2' d)))) (seq (ia one int i) (hide I' X)))) *)
(* Goal: forall d : D, @eq proc (hide I' (Y2 d)) (seq (ia one tau i) (alt (seq (ia one int i) (seq (ia one int i) (hide I' (Y2 d)))) (seq (ia one int i) (hide I' X)))) *)
auto.
3: exact i.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
pattern B at 1 in |- *.
elim Specificat.
pattern B at 1 in |- *.
elim Specificat.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
intro.
pattern X at 1 in |- *.
elim Lem1.
elim (SUM8 D (fun d : D => seq (ia D r1 d) (X1 d)) I').
elim (SUM8 D (fun d : D => hide I' (seq (ia D r1 d) (X1 d))) I'').
elimtype
 ((fun d : D =>
   seq (ia D r1 d)
     (seq (ia D s4 d)
        (D +
         (fun d0 : D =>
          seq (ia D r1 d0) (seq (ia D s4 d0) (hide I'' (hide I' X))))))) =
  (fun d : D => hide I'' (hide I' (seq (ia D r1 d) (X1 d))))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
apply EXTE. intro.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
elim LemLin2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
elimtype
 (seq (ia D r1 d0) (seq (ia one tau i) (hide I'' (X1' d0))) =
  seq (ia D r1 d0) (hide I'' (X1' d0))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
2: apply sym_equal.
2: apply T1'.
elim KFlin2.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
elim LemLin3.

(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
elim KFlin3.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
elim Lem2.
elim (SUM8 D (fun d : D => seq (ia D r1 d) (Y1 d)) I').
elim (SUM8 D (fun d : D => hide I' (seq (ia D r1 d) (Y1 d))) I'').

elimtype
 ((fun d0 : D => seq (ia D r1 d0) (seq (ia D s4 d0) (hide I'' (hide I' X)))) =
  (fun d : D => hide I'' (hide I' (seq (ia D r1 d) (Y1 d))))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
(* Goal: forall d : D, @eq proc (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) (seq (ia one tau i) (hide I'' (Y1' d))) *)
apply EXTE. intro.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
elim LemLin5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'. 
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1.
elimtype
 (seq (ia D r1 d1) (seq (ia one tau i) (hide I'' (Y1' d1))) =
  seq (ia D r1 d1) (hide I'' (Y1' d1))).
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (Y2' d))) *)
2: apply sym_equal.
2: apply T1'.

elim KFlin5. 
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'. 
elim LemLin6.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (seq (ia one int i) (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
elim TI5.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (seq (hide I'' (ia D s4 d)) (hide I'' (hide I' (Y2 d)))))) (seq (ia one tau i) (seq (ia D s4 d) (hide I'' (hide I' (Y2 d))))) *)
(* Goal: In_ehlist int I'' *)
elim TI1. 
elim KFlin6.
(* Goal: @eq proc (seq (ia one tau i) (seq (ia one tau i) (hide I'' (hide I' X)))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
elim T1'.
(* Goal: @eq proc (seq (ia one tau i) (hide I'' (hide I' X))) (seq (ia one tau i) (hide I'' (hide I' X))) *)
(* Goal: In_ehlist int I'' *)
apply refl_equal.
exact IntauI''.
exact Inr1I''.
exact Inr1I.
exact IntauI''.
exact Inr1I''.
exact Inr1I.
 
Save Hurrah.
