(* 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_defs.v                                *)
(****************************************************************************)

Require Import abp_base.

(* HERE STARTS THE APPLICATION SECTION *) 

(* First we define the datatypes with a number of
   elementary axioms about them *)

Section BOOL.
Variable b : bool.
Parameter andb orb : bool -> bool -> bool.
Parameter notb : bool -> bool.
Axiom andb1 : b = andb true b.
Axiom andb2 : false = andb false b.
Axiom orb1 : true = orb true b.
Axiom orb2 : b = orb false b.
Axiom notb1 : false = notb true.
Axiom notb2 : true = notb false.
End BOOL.

Section BIT.
Parameter bit : Set.
Parameter e0 e1 : bit. 
Parameter eqb : bit -> bit -> bool.
Parameter toggle : bit -> bit.
Variable b : bit.
Axiom Toggle1 : e1 = toggle e0.
Axiom Toggle2 : e0 = toggle e1.
Axiom bit1 : true = eqb b b.
Axiom bit2 : false = eqb b (toggle b). 
Axiom bit3 : false = eqb (toggle b) b.
End BIT.

Section DATA.
Parameter D : Set.
Parameter eqD : D -> D -> bool.
Parameter ifD : bool -> D -> D -> D.
Variable d e : D.
Axiom eqD5 : d = ifD true d e.
Axiom eqD6 : e = ifD false d e.
Axiom eqD7 : true = eqD d d.
Axiom eqD8 : ifD (eqD d e) d e = e.

Axiom EQDi : ~ EQ D one.
End DATA.

Goal forall d e : D, d = e -> true = eqD d e.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq bool true (eqD d d) *)
apply eqD7.

Save eqD_elim.

Goal forall d e : D, true = eqD d e -> d = e.

(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq D d e *)
elim (eqD8 d e).
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq D d (ifD true d e) *)
elim eqD5.
(* Goal: @eq act int int *)
apply refl_equal.
Save eqD_intro.

Goal forall d e : D, false = eqD d e -> d <> e.

(* Goal: forall _ : L true, L false *)
intros.
(* Goal: not (@eq Frame d e) *)
red in |- *; intro.
(* Goal: False *)
cut (forall P : bool -> Prop, P true -> P false); intro L.
apply
 (L
    (fun P : bool =>
     match P return Prop with
     | true => True
     | false => False
     end)).
(* Goal: True *)
(* Goal: forall _ : L true, L false *)
exact I.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: L false *)
elimtype (eqD d e = false).
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
elim H0.
(* Goal: L (eqD d d) *)
(* Goal: @eq bool (eqD d e) false *)
elim eqD7.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
(* Goal: @eq act int tau *)
(* Goal: forall _ : False, False *)
apply sym_equal.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
Save eqD_intro'.

Section FRAME1.
Parameter frame : Set.
Variable b b1 b2 : bit.
Variable d e : frame.
Parameter tuple : bit -> frame. 
Parameter sce : frame.
Parameter eqf : frame -> frame -> bool.
Parameter iff : bool -> frame -> frame -> frame.
Axiom eqf1 : true = eqf sce sce.
Axiom eqf2 : false = eqf sce (tuple b).
Axiom eqf3 : false = eqf (tuple b) sce.
Axiom eqf4 : eqb b1 b2 = eqf (tuple b1) (tuple b2).

Axiom eqf5 : d = iff true d e.
Axiom eqf6 : e = iff false d e.
Axiom eqf7 : true = eqf d d.
Axiom eqf8 : iff (eqf d e) d e = e.

Axiom EQfi : ~ EQ frame one.
Axiom EQfD : ~ EQ frame D.
End FRAME1.

 
Goal forall d e : frame, d = e -> true = eqf d e.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq bool true (eqf d d) *)
apply eqf7.
 
Save eqf_elim.
 
Goal forall d e : frame, true = eqf d e -> d = e.
 
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq frame d e *)
elim (eqf8 d e).
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq frame d (iff true d e) *)
elim eqf5.
(* Goal: @eq act int int *)
apply refl_equal.
Save eqf_intro.
 
Goal forall d e : frame, false = eqf d e -> d <> e.
 
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: not (@eq Frame d e) *)
red in |- *; intro.
(* Goal: False *)
cut (forall P : bool -> Prop, P true -> P false); intro L.
apply
 (L
    (fun P : bool =>
     match P return Prop with
     | true => True
     | false => False
     end)).
(* Goal: True *)
(* Goal: forall _ : L true, L false *)
exact I.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: L false *)
elimtype (eqf d e = false).
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
elim H0.
(* Goal: L (eqf d d) *)
(* Goal: @eq bool (eqf d e) false *)
elim eqf7.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
(* Goal: @eq act int tau *)
(* Goal: forall _ : False, False *)
apply sym_equal.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
Save eqf_intro'.
 

Section FRAME2.
Parameter Frame : Set.
Variable b b1 b2 : bit.
Variable d d1 d2 : D.

Variable e e' : Frame.
Parameter Tuple : bit -> D -> Frame. 
Parameter lce : Frame.
Parameter eqF : Frame -> Frame -> bool.
Parameter ifF : bool -> Frame -> Frame -> Frame. 
Axiom eqF1 : true = eqF lce lce.
Axiom eqF2 : false = eqF lce (Tuple b d).
Axiom eqF3 : false = eqF (Tuple b d) lce.
Axiom eqF4 : andb (eqb b1 b2) (eqD d1 d2) = eqF (Tuple b1 d1) (Tuple b2 d2).
 
Axiom eqF5 : e' = ifF true e' e.
Axiom eqF6 : e = ifF false e' e. 
Axiom eqF7 : true = eqF e e. 
Axiom eqF8 : ifF (eqF e e') e e' = e'. 
 
Axiom EQFi : ~ EQ Frame one.
Axiom EQFD : ~ EQ Frame D.
Axiom EQFf : ~ EQ Frame frame.
End FRAME2.


Hint Resolve EQFf (*EQfF*).

Goal forall d e : Frame, d = e -> true = eqF d e.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq bool true (eqF d d) *)
apply eqF7.

Save eqF_elim.

Goal forall d e : Frame, true = eqF d e -> d = e.

(* Goal: forall _ : L true, L false *)
intros.
(* Goal: @eq Frame d e *)
elim (eqF8 d e).
(* Goal: @eq Frame d (ifF (eqF d e) d e) *)
elim H.
(* Goal: @eq Frame d (ifF true d e) *)
elim eqF5.
(* Goal: @eq act int int *)
apply refl_equal.
Save eqF_intro.

Goal forall d e : Frame, false = eqF d e -> d <> e.

(* Goal: forall _ : L true, L false *)
intros.
(* Goal: not (@eq Frame d e) *)
red in |- *; intro.
(* Goal: False *)
cut (forall P : bool -> Prop, P true -> P false); intro L.
apply
 (L
    (fun P : bool =>
     match P return Prop with
     | true => True
     | false => False
     end)).
(* Goal: True *)
(* Goal: forall _ : L true, L false *)
exact I.
(* Goal: forall _ : L true, L false *)
intros.
(* Goal: L false *)
elimtype (eqF d e = false).
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
elim H0.
(* Goal: L (eqF d d) *)
(* Goal: @eq bool (eqF d e) false *)
elim eqF7.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
(* Goal: @eq act int tau *)
(* Goal: forall _ : False, False *)
apply sym_equal.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
assumption.
Save eqF_intro'.
 
(* Below the processes used in the alternating bit protocol
   are defined *)

Parameter K : one -> proc.
Parameter L : one -> proc.
Parameter S : one -> proc.
Parameter Sn : bit -> proc.
Parameter Sn_d : D -> bit -> proc.
Parameter Tn_d : D -> bit -> proc.
Parameter R : one -> proc.
Parameter Rn : bit -> proc.

Section PROC.
Variable b : bit.
Variable j : one.
Variable d : D.

Axiom
  ChanK :
    Frame +
    (fun x : Frame =>
     seq (ia Frame r2 x)
       (seq
          (alt (seq (ia one int i) (ia Frame s3 x))
             (seq (ia one int i) (ia Frame s3 lce))) 
          (K i))) = K j.

Axiom
  ChanL :
    frame +
    (fun n : frame =>
     seq (ia frame r5 n)
       (seq
          (alt (seq (ia one int i) (ia frame s6 n))
             (seq (ia one int i) (ia frame s6 sce))) 
          (L i))) = L j.

Axiom ProcS : seq (Sn e0) (seq (Sn e1) (S i)) = S j.

Axiom ProcSn : D + (fun d : D => seq (ia D r1 d) (Sn_d d b)) = Sn b.

Axiom ProcSn_d : seq (ia Frame s2 (Tuple b d)) (Tn_d d b) = Sn_d d b.

Axiom
  ProcTn_d :
    alt
      (seq (alt (ia frame r6 (tuple (toggle b))) (ia frame r6 sce))
         (Sn_d d b)) (ia frame r6 (tuple b)) = Tn_d d b.

Axiom ProcR : seq (Rn e1) (seq (Rn e0) (R i)) = R j.

Axiom
  ProcRn :
    alt
      (seq
         (alt (D + (fun d : D => ia Frame r3 (Tuple b d))) (ia Frame r3 lce))
         (seq (ia frame s5 (tuple b)) (Rn b)))
      (D +
       (fun d : D =>
        seq (ia Frame r3 (Tuple (toggle b) d))
          (seq (ia D s4 d) (ia frame s5 (tuple (toggle b)))))) = 
    Rn b.
End PROC.

Definition H :=
  ehcons r2
    (ehcons r3
       (ehcons r5
          (ehcons r6 (ehcons s2 (ehcons s3 (ehcons s5 (ehcons s6 ehnil))))))).

Definition ABP := enc H (mer (S i) (mer (K i) (mer (L i) (R i)))).
Definition X := enc H (mer (S i) (mer (K i) (mer (L i) (R i)))).

Definition X1 (d : D) :=
  enc H
    (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (R i)))).

Definition X2 (d : D) :=
  enc H
    (mer (seq (Tn_d d e0) (seq (Sn e1) (S i)))
       (mer (K i)
          (mer (L i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))).

Definition Y :=
  enc H (mer (seq (Sn e1) (S i)) (mer (K i) (mer (L i) (seq (Rn e0) (R i))))).

Definition Y1 (d : D) :=
  enc H
    (mer (seq (Sn_d d e1) (S i)) (mer (K i) (mer (L i) (seq (Rn e0) (R i))))).

Definition Y2 (d : D) :=
  enc H
    (mer (seq (Tn_d d e1) (S i))
       (mer (K i) (mer (L i) (seq (ia frame s5 (tuple e1)) (R i))))).


(* Here the section on equality of actions starts *)

Goal r1 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1r2.

Goal r1 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1r3. 

Goal r1 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1r5. 

Goal r1 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1r6. 

Goal r1 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1s2.

Goal r1 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1s3.

Goal r1 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1s4.

Goal r1 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1s5.

Goal r1 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1s6.

Goal r1 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1c2.

Goal r1 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1c3.

Goal r1 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1c5.

Goal r1 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1c6.

Goal r1 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1int.

Goal r1 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr1tau.

Hint Resolve neqr1r2 neqr1r3 neqr1r5 neqr1r6 neqr1s2 neqr1s3 neqr1s4 neqr1s5
  neqr1s6 neqr1c2 neqr1c3 neqr1c5 neqr1c6 neqr1int neqr1tau.

Goal r2 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2r1.

Goal r2 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2r3. 

Goal r2 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2r5. 

Goal r2 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2r6. 

Goal r2 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2s2.

Goal r2 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2s3.

Goal r2 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2s4.

Goal r2 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2s5.

Goal r2 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2s6.

Goal r2 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2c2.

Goal r2 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2c3.

Goal r2 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2c5.

Goal r2 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2c6.

Goal r2 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2int.

Goal r2 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr2tau.

Hint Resolve neqr2r1 neqr2r3 neqr2r5 neqr2r6 neqr2s2 neqr2s3 neqr2s4 neqr2s5
  neqr2s6 neqr2c2 neqr2c3 neqr2c5 neqr2c6 neqr2int neqr2tau.


Goal r3 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3r1.

Goal r3 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3r2.

Goal r3 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3r5. 

Goal r3 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3r6. 

Goal r3 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3s2.

Goal r3 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3s3.

Goal r3 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3s4.

Goal r3 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3s5.

Goal r3 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3s6.

Goal r3 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3c2.

Goal r3 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3c3.

Goal r3 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3c5.

Goal r3 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3c6.

Goal r3 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3int.

Goal r3 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr3tau.

Hint Resolve neqr3r2 neqr3r1 neqr3r5 neqr3r6 neqr3s2 neqr3s3 neqr3s4 neqr3s5
  neqr3s6 neqr3c2 neqr3c3 neqr3c5 neqr3c6 neqr3int neqr3tau.


Goal r5 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5r1.

Goal r5 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5r2.

Goal r5 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5r3. 

Goal r5 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5r6. 

Goal r5 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5s2.

Goal r5 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5s3.

Goal r5 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5s4.

Goal r5 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5s5.

Goal r5 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5s6.

Goal r5 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5c2.

Goal r5 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5c3.

Goal r5 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5c5.

Goal r5 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5c6.

Goal r5 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5int.

Goal r5 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr5tau.

Hint Resolve neqr5r2 neqr5r3 neqr5r1 neqr5r6 neqr5s2 neqr5s3 neqr5s4 neqr5s5
  neqr5s6 neqr5c2 neqr5c3 neqr5c5 neqr5c6 neqr5int neqr5tau.


Goal r6 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6r1.

Goal r6 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6r2.

Goal r6 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6r3. 

Goal r6 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6r5. 

Goal r6 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6s2.

Goal r6 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6s3.

Goal r6 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6s4.

Goal r6 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6s5.

Goal r6 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6s6.

Goal r6 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6c2.

Goal r6 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6c3.

Goal r6 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6c5.

Goal r6 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6c6.

Goal r6 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6int.

Goal r6 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqr6tau.

Hint Resolve neqr6r2 neqr6r3 neqr1r5 neqr6r1 neqr6s2 neqr6s3 neqr6s4 neqr6s5
  neqr6s6 neqr6c2 neqr6c3 neqr6c5 neqr6c6 neqr6int neqr6tau.


Goal s2 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2r1.

Goal s2 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2r2.

Goal s2 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2r3. 

Goal s2 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2r5. 

Goal s2 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2r6. 

Goal s2 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2s3.

Goal s2 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2s4.

Goal s2 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2s5.

Goal s2 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2s6.

Goal s2 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2c2.

Goal s2 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2c3.

Goal s2 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2c5.

Goal s2 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2c6.

Goal s2 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2int.

Goal s2 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs2tau.

Hint Resolve neqs2r2 neqs2r3 neqs2r5 neqs2r6 neqs2r1 neqs2s3 neqs2s4 neqs2s5
  neqs2s6 neqs2c2 neqs2c3 neqs2c5 neqs2c6 neqs2int neqs2tau.

Goal s3 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3r1.

Goal s3 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3r2.

Goal s3 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3r3. 

Goal s3 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3r5. 

Goal s3 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3r6. 

Goal s3 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3s2.

Goal s3 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3s4.

Goal s3 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3s5.

Goal s3 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3s6.

Goal s3 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3c2.

Goal s3 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3c3.

Goal s3 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3c5.

Goal s3 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3c6.

Goal s3 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3int.

Goal s3 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs3tau.

Hint Resolve neqs3r2 neqs3r3 neqs3r5 neqs3r6 neqs3s2 neqs3s4 neqs3s5 neqs3s6
  neqs3c2 neqs3c3 neqs3c5 neqs3c6 neqs3int neqs3tau.


Goal s4 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4r1.

Goal s4 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4r2.

Goal s4 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4r3. 

Goal s4 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4r5. 

Goal s4 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4r6. 

Goal s4 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4s2.

Goal s4 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4s3.

Goal s4 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4s5.

Goal s4 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4s6.

Goal s4 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4c2.

Goal s4 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4c3.

Goal s4 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4c5.

Goal s4 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4c6.

Goal s4 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4int.

Goal s4 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs4tau.

Hint Resolve neqs4r2 neqs4r3 neqs4r5 neqs4r6 neqs4s2 neqs4s3 neqs4s5 neqs4s6
  neqs4c2 neqs4c3 neqs4c5 neqs4c6 neqs4int neqs4tau.


Goal s5 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5r1.

Goal s5 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5r2.

Goal s5 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5r3. 

Goal s5 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5r5. 

Goal s5 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5r6. 

Goal s5 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5s2.

Goal s5 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5s3.

Goal s5 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5s4.

Goal s5 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5s6.

Goal s5 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5c2.

Goal s5 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5c3.

Goal s5 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5c5.

Goal s5 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5c6.

Goal s5 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5int.

Goal s5 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs5tau.

Hint Resolve neqs5r2 neqs5r3 neqs5r5 neqs5r6 neqs5s2 neqs5s3 neqs5s4 neqs5r1
  neqs5s6 neqr1c2 neqs5c3 neqs5c5 neqs5c6 neqs5int neqs5tau.

Goal s6 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6r1.

Goal s6 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6r2.

Goal s6 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6r3. 

Goal s6 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6r5. 

Goal s6 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6r6. 

Goal s6 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6s2.

Goal s6 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6s3.

Goal s6 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6s4.

Goal s6 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6s5.

Goal s6 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6c2.

Goal s6 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6c3.

Goal s6 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6c5.

Goal s6 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6c6.

Goal s6 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6int.

Goal s6 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqs6tau.

Hint Resolve neqs6r2 neqs6r3 neqs6r5 neqs6r6 neqs6s2 neqs6s3 neqs6s4 neqs6s5
  neqs6r1 neqs6c2 neqs6c3 neqs6c5 neqs6c6 neqs6int neqs6tau.


Goal c2 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2r1.

Goal c2 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2r2.

Goal c2 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2r3. 

Goal c2 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2r5. 

Goal c2 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2r6. 

Goal c2 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2s2.

Goal c2 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2s3.

Goal c2 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2s4.

Goal c2 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2s5.

Goal c2 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2s6.

Goal c2 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2c3.

Goal c2 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2c5.

Goal c2 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc1c6.

Goal c2 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2int.

Goal c2 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc2tau.

Hint Resolve neqc2r2 neqc2r3 neqc2r5 neqc2r6 neqc2s2 neqc2s3 neqc2s4 neqc2s5
  neqc2s6 neqc2c3 neqc2c5 (*neqc2c6*)  neqc2int neqc2tau.

Goal c3 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3r1.

Goal c3 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3r2.

Goal c3 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3r3. 

Goal c3 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3r5. 

Goal c3 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3r6. 

Goal c3 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3s2.

Goal c3 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3s3.

Goal c3 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3s4.

Goal c3 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3s5.

Goal c3 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3s6.

Goal c3 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3c2.

Goal c3 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3c5.

Goal c3 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3c6.

Goal c3 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3int.

Goal c3 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc3tau.

Hint Resolve neqc3r2 neqc3r3 neqc3r5 neqc3r6 neqc3s2 neqc3s3 neqc3s4 neqc3s5
  neqc3s6 neqc3c2 neqc3r1 neqc3c5 neqc3c6 neqc3int neqc3tau.


Goal c5 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5r1.

Goal c5 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5r2.

Goal c5 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5r3. 

Goal c5 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5r5. 

Goal c5 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5r6. 

Goal c5 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5s2.

Goal c5 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5s3.

Goal c5 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5s4.

Goal c5 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5s5.

Goal c5 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5s6.

Goal c5 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5c2.

Goal c5 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5c3.

Goal c5 <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5c6.

Goal c5 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5int.

Goal c5 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc5tau.

Hint Resolve neqc5r2 neqc5r3 neqc5r5 neqc5r6 neqc5s2 neqc5s3 neqc5s4 neqc5s5
  neqc5s6 neqc5c2 neqc5c3 neqc5r1 neqc5c6 neqc5int neqc5tau.


Goal c6 <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6r1.

Goal c6 <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6r2.

Goal c6 <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6r3. 

Goal c6 <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6r5. 

Goal c6 <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6r6. 

Goal c6 <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6s2.

Goal c6 <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6s3.

Goal c6 <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6s4.

Goal c6 <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6s5.

Goal c6 <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6s6.

Goal c6 <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6c2.

Goal c6 <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6c3.

Goal c6 <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6c5.

Goal c6 <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6int.

Goal c6 <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqc6tau.

Hint Resolve neqc6r2 neqc6r3 neqc6r5 neqc6r6 neqc6s2 neqc6s3 neqc6s4 neqc6s5
  neqc6s6 neqc6c2 neqc6c3 neqc6c5 neqc6r1 neqc6int neqc6tau.


Goal int <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintr1.

Goal int <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintr2.

Goal int <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintr3. 

Goal int <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintr5. 

Goal int <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintr6. 

Goal int <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqints2.

Goal int <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqints3.

Goal int <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqints4.

Goal int <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqints5.

Goal int <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqints6.

Goal int <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintc2.

Goal int <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintc3.

Goal int <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintc5.

Goal int <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqintc6.

Goal int <> tau.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqinttau.

Hint Resolve neqintr2 neqintr3 neqintr5 neqintr6 neqints2 neqints3 neqints4
  neqints5 neqints6 neqintc2 neqintc3 neqintc5 neqintc6 neqintr1 neqinttau.


Goal tau <> r1.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaur1.

Goal tau <> r2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaur2.

Goal tau <> r3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaur3. 

Goal tau <> r5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaur5. 

Goal tau <> r6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaur6. 

Goal tau <> s2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaus2.

Goal tau <> s3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaus3.

Goal tau <> s4.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaus4.

Goal tau <> s5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaus5.

Goal tau <> s6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtaus6.

Goal tau <> c2.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtauc2.

Goal tau <> c3.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtauc3.

Goal tau <> c5.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtauc5.

Goal tau <> c6.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtauc6.

Goal tau <> int.
(* Goal: not (@eq act tau int) *)
discriminate.
Save neqtauint.

Hint Resolve neqtaur2 neqtaur3 neqtaur5 neqtaur6 neqtaus2 neqtaus3 neqtaus4
  neqtaus5 neqtaus6 neqtauc2 neqtauc3 neqtauc5 neqtauc6 neqtauint neqtaur1.

(*Here the section on equality of actions ends *)

(*Here the section on actions in the set H starts *)

Goal forall a : act, a = r2 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: In_ehlist s6 H *)
auto.
Save HLemmar2.

Goal forall a : act, a = r3 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: In_ehlist s6 H *)
auto.
Save HLemmar3.

Goal forall a : act, a = r5 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: In_ehlist s6 H *)
auto.
Save HLemmar5.

Goal forall a : act, a = r6 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: In_ehlist s6 H *)
auto.
Save HLemmar6.

Goal forall a : act, a = s2 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: or (@eq act a r2) (or (@eq act a r3) (or (@eq act a r5) (or (@eq act a r6) (or (@eq act a s2) (or (@eq act a s3) (or (@eq act a s5) (or (@eq act a s6) False))))))) *)
auto 10.
Save HLemmas2.

Goal forall a : act, a = s3 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: or (@eq act a r2) (or (@eq act a r3) (or (@eq act a r5) (or (@eq act a r6) (or (@eq act a s2) (or (@eq act a s3) (or (@eq act a s5) (or (@eq act a s6) False))))))) *)
auto 10.
Save HLemmas3.

Goal forall a : act, a = s5 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: or (@eq act a r2) (or (@eq act a r3) (or (@eq act a r5) (or (@eq act a r6) (or (@eq act a s2) (or (@eq act a s3) (or (@eq act a s5) (or (@eq act a s6) False))))))) *)
auto 10.
Save HLemmas5.

Goal forall a : act, a = s6 -> In_ehlist a H.
(* Goal: forall (a : act) (_ : @eq act a s6), In_ehlist a H *)
intros a b.
(* Goal: forall _ : In_ehlist a H, False *)
unfold In_ehlist, H in |- *.
(* Goal: or (@eq act a r2) (or (@eq act a r3) (or (@eq act a r5) (or (@eq act a r6) (or (@eq act a s2) (or (@eq act a s3) (or (@eq act a s5) (or (@eq act a s6) False))))))) *)
auto 10.
Save HLemmas6.


Goal
forall a : act,
a <> r2 ->
a <> r3 ->
a <> r5 ->
a <> r6 -> a <> s2 -> a <> s3 -> a <> s5 -> a <> s6 -> ~ In_ehlist a H.
(* Goal: forall (a : act) (_ : not (@eq act a r2)) (_ : not (@eq act a r3)) (_ : not (@eq act a r5)) (_ : not (@eq act a r6)) (_ : not (@eq act a s2)) (_ : not (@eq act a s3)) (_ : not (@eq act a s5)) (_ : not (@eq act a s6)), not (In_ehlist a H) *)
intros a b b0 b1 b2 b3 b4 b5 b6.
(* Goal: forall _ : In_ehlist a H, False *)
red in |- *. unfold In_ehlist, H in |- *. 
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I1. elim I1. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I2. elim I2. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I3. elim I3. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I4. elim I4. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I5. elim I5. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I6. elim I6. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I7. elim I7. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro I8. elim I8. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro. assumption.
Save HLemma.

Hint Resolve HLemmar2 HLemmar3 HLemmar5 HLemmar6 HLemmas2 HLemmas3 HLemmas5
  HLemmas6 HLemma.

Goal ~ In_ehlist r1 H.
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Inr1H.

Goal In_ehlist r2 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Inr2H.

Goal In_ehlist r3 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Inr3H.

Goal In_ehlist r5 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Inr5H.

Goal In_ehlist r6 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Inr6H.

Goal In_ehlist s2 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Ins2H.

Goal In_ehlist s3 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Ins3H.

Goal ~ In_ehlist s4 H.
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Ins4H.

Goal In_ehlist s5 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Ins5H.

Goal In_ehlist s6 H.
(* Goal: In_ehlist s6 H *)
auto.
Save Ins6H.

Goal ~ In_ehlist int H.
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save InintH.

Goal ~ In_ehlist c2 H.
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Inc2H.

Goal ~ In_ehlist c3 H. 
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Inc3H. 

Goal ~ In_ehlist c5 H. 
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Inc5H. 

Goal ~ In_ehlist c6 H. 
(* Goal: In_ehlist s6 H *)
apply HLemma; auto.
Save Inc6H. 

Definition I' := ehcons c2 (ehcons c3 (ehcons c5 (ehcons c6 ehnil))).
Definition I'' := ehcons int ehnil.

Goal In_ehlist c2 I'.
(* Goal: forall _ : In_ehlist r1 I', False *)
unfold In_ehlist, I' in |- *. 
(* Goal: @eq act int int *)
left; apply refl_equal. 
Save Inc2I. 

Goal In_ehlist c3 I'.
(* Goal: forall _ : In_ehlist r1 I', False *)
unfold In_ehlist, I' in |- *. 
(* Goal: @eq act int int *)
right; left; apply refl_equal. 
Save Inc3I. 

Goal In_ehlist c5 I'.
(* Goal: forall _ : In_ehlist r1 I', False *)
unfold In_ehlist, I' in |- *. 
(* Goal: @eq act int int *)
right; right; left; apply refl_equal. 
Save Inc5I. 

Goal In_ehlist c6 I'.
(* Goal: forall _ : In_ehlist r1 I', False *)
unfold In_ehlist, I' in |- *.
(* Goal: @eq act int int *)
right; right; right; left; apply refl_equal.
Save Inc6I.

Goal ~ In_ehlist int I'.
(* Goal: not (In_ehlist s4 I'') *)
red in |- *. unfold In_ehlist, I' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqintc2. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H1. intro. apply neqintc3. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H2. intro. apply neqintc5. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H3. intro. apply neqintc6. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; assumption.
Save InintI.

Goal ~ In_ehlist s4 I'.
(* Goal: not (In_ehlist s4 I'') *)
red in |- *. unfold In_ehlist, I' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqs4c2. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H1. intro. apply neqs4c3. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H2. intro. apply neqs4c5. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H3. intro. apply neqs4c6. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; assumption.
Save Ins4I.

Goal ~ In_ehlist r1 I'.
(* Goal: not (In_ehlist s4 I'') *)
red in |- *. unfold In_ehlist, I' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqr1c2. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H1. intro. apply neqr1c3. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H2. intro. apply neqr1c5. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; elim H3. intro. apply neqr1c6. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; assumption.
Save Inr1I.

Goal In_ehlist int I''.
(* Goal: forall _ : In_ehlist s4 I'', False *)
unfold In_ehlist, I'' in |- *.
(* Goal: @eq act int int *)
left. apply refl_equal.
Save InintI''.


Goal ~ In_ehlist s4 I''.
(* Goal: not (In_ehlist s4 I'') *)
red in |- *. unfold In_ehlist, I'' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqints4. 
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
apply sym_equal. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro. assumption.
Save Ins4I''.

Goal ~ In_ehlist r1 I''.
(* Goal: forall _ : In_ehlist s4 I'', False *)
red in |- *; unfold In_ehlist, I'' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqintr1. 
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
apply sym_equal. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; assumption.
Save Inr1I''.

Goal ~ In_ehlist tau I''.
(* Goal: forall _ : In_ehlist s4 I'', False *)
red in |- *; unfold In_ehlist, I'' in |- *.
(* Goal: L (eqF d e) *)
(* Goal: @eq bool (eqF d e) false *)
intro; elim H0. intro. apply neqinttau. 
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
apply sym_equal. assumption.
(* Goal: @eq act tau int *)
(* Goal: forall _ : False, False *)
intro; assumption.
Save IntauI''.

(*  End of basic axioms about the sets H and I   *)