Skip to content

Instantly share code, notes, and snippets.

@SkySkimmer

SkySkimmer/00script.v

Last active July 31, 2024 11:13
Show Gist options
  • Save SkySkimmer/10e39d6672a79d53f0932cbe33ebe2c8 to your computer and use it in GitHub Desktop.
Save SkySkimmer/10e39d6672a79d53f0932cbe33ebe2c8 to your computer and use it in GitHub Desktop.
Download ZIP
bug in use of sharing analysis
Raw
00script.v
Inductive T :=
| C1 (_ _ : T)
| C2 (_ _ : T).
Set Debug "hcons-before-hconstr".
(* or run coqchk on the result *)
Lemma foo (x y:T) : {x=y} + {x<>y}.
Proof.
decide equality.
Qed. (* Anomaly "hconstr sharing_info mismatch at idx 42" Please report at http://coq.inria.fr/bugs/. *)
Raw
01proof term
(fun x y : T =>
T_rec (fun x0 : T => forall x1 : T, sumbool (@eq T x0 x1) (not (@eq T x0 x1)))
(fun (t : T) (H : forall x0 : T, sumbool (@eq T t x0) (not (@eq T t x0)))
(t0 : T) (H0 : forall x0 : T, sumbool (@eq T t0 x0) (not (@eq T t0 x0)))
(x0 : T) =>
match x0 as t1 return (sumbool (@eq T (C1 t t0) t1) (not (@eq T (C1 t t0) t1))) with
| C1 t1 t2 =>
(fun t3 t4 : T =>
@sumbool_rec (@eq T t t3) (not (@eq T t t3))
(fun _ : sumbool (@eq T t t3) (not (@eq T t t3)) =>
sumbool (@eq T (C1 t t0) (C1 t3 t4)) (not (@eq T (C1 t t0) (C1 t3 t4))))
(fun a : @eq T t t3 =>
@sumbool_rec (@eq T t0 t4) (not (@eq T t0 t4))
(fun _ : sumbool (@eq T t0 t4) (not (@eq T t0 t4)) =>
sumbool (@eq T (C1 t t0) (C1 t3 t4)) (not (@eq T (C1 t t0) (C1 t3 t4))))
(fun a0 : @eq T t0 t4 =>
@left (@eq T (C1 t t0) (C1 t3 t4)) (not (@eq T (C1 t t0) (C1 t3 t4)))
(@eq_ind_r T t3 (fun t5 : T => @eq T (C1 t5 t0) (C1 t3 t4))
(@eq_ind_r T t4 (fun t5 : T => @eq T (C1 t3 t5) (C1 t3 t4))
(@eq_refl T (C1 t3 t4)) t0 a0) t a))
(fun diseq : not (@eq T t0 t4) =>
@right (@eq T (C1 t t0) (C1 t3 t4)) (not (@eq T (C1 t t0) (C1 t3 t4)))
(@eq_ind_r T t3 (fun t5 : T => not (@eq T (C1 t5 t0) (C1 t3 t4)))
((fun absurd : @eq T (C1 t3 t0) (C1 t3 t4) =>
diseq
(let H1 : @eq T t0 t4 :=
@f_equal T T
(fun e : T => match e return T with
| C1 _ t5 => t5
| C2 _ _ => t0
end) (C1 t3 t0) (C1 t3 t4) absurd in
(fun H2 : @eq T t0 t4 => H2) H1))
:
not (@eq T (C1 t3 t0) (C1 t3 t4))) t a)) (H0 t4))
(fun diseq : not (@eq T t t3) =>
@right (@eq T (C1 t t0) (C1 t3 t4)) (not (@eq T (C1 t t0) (C1 t3 t4)))
((fun absurd : @eq T (C1 t t0) (C1 t3 t4) =>
diseq
(let H1 : @eq T t t3 :=
@f_equal T T
(fun e : T => match e return T with
| C1 t5 _ => t5
| C2 _ _ => t
end) (C1 t t0) (C1 t3 t4) absurd in
(let H2 : @eq T t0 t4 :=
@f_equal T T
(fun e : T => match e return T with
| C1 _ t5 => t5
| C2 _ _ => t0
end) (C1 t t0) (C1 t3 t4) absurd in
(fun (_ : @eq T t0 t4) (H3 : @eq T t t3) => H3) H2) H1))
:
not (@eq T (C1 t t0) (C1 t3 t4)))) (H t3)) t1 t2
| C2 t1 t2 =>
(fun t3 t4 : T =>
@right (@eq T (C1 t t0) (C2 t3 t4)) (not (@eq T (C1 t t0) (C2 t3 t4)))
((fun H1 : @eq T (C1 t t0) (C2 t3 t4) =>
let H2 : False :=
@eq_ind T (C1 t t0)
(fun e : T => match e return Prop with
| C1 _ _ => True
| C2 _ _ => False
end) I (C2 t3 t4) H1 in
False_ind False H2)
:
not (@eq T (C1 t t0) (C2 t3 t4)))) t1 t2
end)
(fun (t : T) (H : forall x0 : T, sumbool (@eq T t x0) (not (@eq T t x0)))
(t0 : T) (H0 : forall x0 : T, sumbool (@eq T t0 x0) (not (@eq T t0 x0)))
(x0 : T) =>
match x0 as t1 return (sumbool (@eq T (C2 t t0) t1) (not (@eq T (C2 t t0) t1))) with
| C1 t1 t2 =>
(fun t3 t4 : T =>
@right (@eq T (C2 t t0) (C1 t3 t4)) (not (@eq T (C2 t t0) (C1 t3 t4)))
((fun H1 : @eq T (C2 t t0) (C1 t3 t4) =>
let H2 : False :=
@eq_ind T (C2 t t0)
(fun e : T => match e return Prop with
| C1 _ _ => False
| C2 _ _ => True
end) I (C1 t3 t4) H1 in
False_ind False H2)
:
not (@eq T (C2 t t0) (C1 t3 t4)))) t1 t2
| C2 t1 t2 =>
(fun t3 t4 : T =>
@sumbool_rec (@eq T t t3) (not (@eq T t t3))
(fun _ : sumbool (@eq T t t3) (not (@eq T t t3)) =>
sumbool (@eq T (C2 t t0) (C2 t3 t4)) (not (@eq T (C2 t t0) (C2 t3 t4))))
(fun a : @eq T t t3 =>
@sumbool_rec (@eq T t0 t4) (not (@eq T t0 t4))
(fun _ : sumbool (@eq T t0 t4) (not (@eq T t0 t4)) =>
sumbool (@eq T (C2 t t0) (C2 t3 t4)) (not (@eq T (C2 t t0) (C2 t3 t4))))
(fun a0 : @eq T t0 t4 =>
@left (@eq T (C2 t t0) (C2 t3 t4)) (not (@eq T (C2 t t0) (C2 t3 t4)))
(@eq_ind_r T t3 (fun t5 : T => @eq T (C2 t5 t0) (C2 t3 t4))
(@eq_ind_r T t4 (fun t5 : T => @eq T (C2 t3 t5) (C2 t3 t4))
(@eq_refl T (C2 t3 t4)) t0 a0) t a))
(fun diseq : not (@eq T t0 t4) =>
@right (@eq T (C2 t t0) (C2 t3 t4)) (not (@eq T (C2 t t0) (C2 t3 t4)))
(@eq_ind_r T t3 (fun t5 : T => not (@eq T (C2 t5 t0) (C2 t3 t4)))
((fun absurd : @eq T (C2 t3 t0) (C2 t3 t4) =>
diseq
(let H1 : @eq T t0 t4 :=
@f_equal T T
(fun e : T => match e return T with
| C1 _ _ => t0
| C2 _ t5 => t5
end) (C2 t3 t0) (C2 t3 t4) absurd in
(fun H2 : @eq T t0 t4 => H2) H1))
:
not (@eq T (C2 t3 t0) (C2 t3 t4))) t a)) (H0 t4))
(fun diseq : not (@eq T t t3) =>
@right (@eq T (C2 t t0) (C2 t3 t4)) (not (@eq T (C2 t t0) (C2 t3 t4)))
((fun absurd : @eq T (C2 t t0) (C2 t3 t4) =>
diseq
(let H1 : @eq T t t3 :=
@f_equal T T
(fun e : T => match e return T with
| C1 _ _ => t
| C2 t5 _ => t5
end) (C2 t t0) (C2 t3 t4) absurd in
(let H2 : @eq T t0 t4 :=
@f_equal T T
(fun e : T => match e return T with
| C1 _ _ => t0
| C2 _ t5 => t5
end) (C2 t t0) (C2 t3 t4) absurd in
(fun (_ : @eq T t0 t4) (H3 : @eq T t t3) => H3) H2) H1))
:
not (@eq T (C2 t t0) (C2 t3 t4)))) (H t3)) t1 t2
end) x y)
Raw
02annotated proof term
(* 0 *) fun (x:(*1*)T) (*2*)(y : (*S1*)T) =>
(* 3 *) ((*4*)T_rec)
(* 5 *) (fun x0 : (*S1*)T => (*6*)forall x1 : (*S1*)T, (*7*)
(((*8*)sumbool) (*9*)((*10*)@eq (*1*)T (*11*)x0 (*12*)x1)
(*13*)((*14*)not (*S9*)(@eq T x0 x1)))
(*15*)(fun (t : (*S1*)T) (*16*) (H : (*S6*)forall x0 : T, sumbool (@eq T t x0) (not (@eq T t x0)))
(* 17 *) (t0 : (*S1*)T) (*18*)(H0 : (*S6*)forall x0 : T, sumbool (@eq T t0 x0) (not (@eq T t0 x0)))
(*19*)(x0 : (*1*)T) =>
(*20*)match (*S12*)x0 as t1 return (*21*)((*S8*)sumbool (*22*)((*S10*)@eq (*S1*)T (*23*)((*24*)C1 (*25*)t (*26*)t0) (*S12*)t1) (*27*)((*S14*)not (*S22*)(@eq T (C1 t t0) t1))) with
| C1 t1 t2 =>
(*28(app)*)
(*29*)(fun (t3:(*S1*)T) (*30*)(t4 : (*S1*)T) =>
(* 31 *)
((*32*)@sumbool_rec)
(*33*)((*S10*)@eq (*S1*)T (*34*)t (*S11*)t3)
(*35*)((*S14*)not (*S33*)(@eq T t t3))
(*36*)(fun _ : (*37*) ((*S8*)sumbool) (*S33*)(@eq T t t3) (*S35*)(not (@eq T t t3)) =>
(*38*) ((*S8*)sumbool)
(*39*)((*S10*)@eq (*S1*)T (*40*)((*S24*)C1 (*41*)t (*42*)t0) (*43*)((*S24*)C1 (*44*)t3 (*S11*)t4))
(*45*)((*S14*)not (*S39*)(@eq T (C1 t t0) (C1 t3 t4))))
(*46*)(fun a : (*S33*)@eq T t t3 =>
(*47*) ((*S32*)@sumbool_rec)
(*48*)((*S10*)@eq (*S1*)T (*S42*)t0 (*S11*)t4)
(*49*)((*S14*)not (*S48*)(@eq T t0 t4))
(*50*)(fun _ : (*51*) ((*S8*)sumbool) (*S48*)(@eq T t0 t4) (*S49*)(not (@eq T t0 t4)) =>
(*52*) ((*S8*)sumbool)
(*53*)((*S10*)@eq (*S1*)T
(*54*)((*S24*)C1 (*55*)t (*S34*)t0)
(*56*)((*S24*)C1 (*S26*)t3 (*S44*)t4))
(*57*)((*S14*)not (*S53*)(@eq T (C1 t t0) (C1 t3 t4))))
(*58*)(fun a0 : (*S48*)@eq T t0 t4 =>
(*59*) ((*60*)@left)
(*S53*)(@eq T (C1 t t0) (C1 t3 t4))
(*S57*)(not (@eq T (C1 t t0) (C1 t3 t4)))
(*61*)((*62*)@eq_ind_r (*S1*)T (*S26*)t3
(*63*)(fun t5 : (*S1*)T => (*64*) ((*S10*)@eq) (*S1*)T
(*65*)((*S24*)C1 (*S12*)t5 (*S41*)t0)
(*66*)((*S24*)C1 (*67*)t3 (*S26*)t4))
(*68*)((*S62*)@eq_ind_r (*S1*)T (*S44*)t4
(*69*)(fun t5 : (*S1*)T => (*70*) ((*S10*)@eq) (*S1*)T
(*71*)((*S24*)C1 (*S67*)t3 (*S12*)t5)
(*S66*)(C1 t3 t4))
(*72*)((*73*)@eq_refl (*S1*)T (*S56*)(C1 t3 t4))
(*S34*)t0
(*S12*)a0)
(*S55*)t
(*S11*)a))
(*74*)(fun diseq : (*S49*) not (@eq T t0 t4) =>
(*75*) ((*76*)@right)
(*S53*)(@eq T (C1 t t0) (C1 t3 t4))
(*S57*)(not (@eq T (C1 t t0) (C1 t3 t4)))
(*77*)((*S62*)@eq_ind_r (*S1*)T (*S26*)t3
(*78*)(fun t5 : (*S1*)T =>
(*79*) ((*S14*)not) (*S64*)(@eq T (C1 t5 t0) (C1 t3 t4)))
(*80*)((*81*)(fun absurd : (*82*) ((*S10*)@eq) (*S1*)T
(*83*)((*S24*)C1 (*S26*)t3 (*S34*)t0)
(*S56*)(C1 t3 t4) =>
(* 84 *) ((*S11*)diseq)
(*85*) (let H1 : (*92*) ((*S10*)@eq) (*S1*)T (*S41*)t0 (*S26*)t4 :=
(*86*) ((*87*)@f_equal) (*S1*)T (*S1*)T
(*88*) (fun e : (*S1*)T => (*89*)match (*S12*)e return (*S1*)T with
| C1 _ t5 => (*S12*)t5
| C2 _ _ => (*90*)t0
end)
(*91*) ((*S24*)C1 (*S67*)t3 (*S41*)t0)
(*S66*) (C1 t3 t4)
(*S12*) absurd
in
(* 93(app) *)
(* 94 *) (fun H2 : (*95*) ((*S10*)@eq) (*S1*)T (*S55*)t0 (*S67*)t4 =>
(*S12*)H2)
(*S12*)H1))
: (* 96 *)
((*S14*)not) (*S82*)(@eq T (C1 t3 t0) (C1 t3 t4)))
(*S55*)t
(*S11*)a))
(*97*)((*98*)H0 (*S11*)t4))
(*99*)(fun diseq : (*S35*) not (@eq T t t3) =>
(* 100 *)
(*S76*)@right
(*S39*)(@eq T (C1 t t0) (C1 t3 t4))
(*S45*)(not (@eq T (C1 t t0) (C1 t3 t4)))
(*101*) ((*102*)(fun absurd : (*S39*) @eq T (C1 t t0) (C1 t3 t4) =>
(* 103 *)
(*S11*)diseq
(* 104 *) (let H1 : (*109*) ((*S10*)@eq) (*S1*)T (*S55*)t (*S26*)t3 :=
(* 105 *)
(*S87*)@f_equal (*S1*)T (*S1*)T
(*106*) (fun e : (*S1*)T =>
(*107*) match (*S12*)e return (*S1*)T with
| C1 t5 _ => (*S11*)t5
| C2 _ _ => (*108*)t
end)
(*S54*)(C1 t t0)
(*S56*)(C1 t3 t4)
(*S12*)absurd
in
(* 110 (app) *)
(*111*)(let H2 : (*S92*) @eq T t0 t4 :=
(* 112 *)
(*S87*)@f_equal (*S1*)T (*S1*)T
(*S88*)(fun e : T => match e return T with
| C1 _ t5 => t5
| C2 _ _ => t0
end)
(*113*)((*S24*)C1 (*114*)t (*S41*)t0)
(*S66*)(C1 t3 t4)
(*S11*)absurd
in
(* 115 (app) *)
(* 116 *) (fun (_ : (* S95 *) @eq T t0 t4)
(*117*) (H3 : (*118*) ((*S10*)@eq) (*S1*)T (*S108*)t (*S98*)t3) =>
(*S12*)H3)
(*S12*)H2)
(*S12*)H1))
:
(* S45 *) not (@eq T (C1 t t0) (C1 t3 t4))))
(* 119 *) ((*S42*)H (*S11*)t3))
(*S11*)t1
(*S12*)t2
| C2 t1 t2 =>
(* 120 (app) *)
(*121*) (fun (t3:(*S1*)T) (*122*) (t4 : (*S1*)T) =>
(* 123 *)
(*S76*)@right
(*124*) ((*S10*)@eq (*S1*)T
(*125*)((*S24*)C1 (*S34*)t (*S98*)t0)
(*126*)((*127*)C2 (*S11*)t3 (*S12*)t4))
(*128*)((*S14*)not (*S124*)(@eq T (C1 t t0) (C2 t3 t4)))
(*129 (cast)*)
((*130*)(fun H1 : (*S124*) @eq T (C1 t t0) (C2 t3 t4) =>
(* 131 *) let H2 : (*S138*)False :=
(* 132 *)
((*133*)@eq_ind) (*S1*)T (*S40*)(C1 t t0)
(* 134 *) (fun e : (*S1*)T =>
(*135*)match (*S12*)e return (*136*)Prop with
| C1 _ _ => (*137*)True
| C2 _ _ => (*138*)False
end)
(*139*)I
(*140*)((*S127*)C2 (*S44*)t3 (*S11*)t4)
(*S12*)H1
in
(* 141 *)
(* 142 *) False_ind (*S138*)False (*S12*)H2)
:
(* S128*) not (@eq T (C1 t t0) (C2 t3 t4))))
(*S11*)t1
(*S12*)t2
end)
(* 143 *)
(fun (t : (*S1*)T)
(*144*) (H : (*S6*) forall x0 : T, sumbool (@eq T t x0) (not (@eq T t x0)))
(*145*) (t0 : (*S1*)T)
(*146*) (H0 : (*S6*) forall x0 : T, sumbool (@eq T t0 x0) (not (@eq T t0 x0)))
(*147*) (x0 : (*S1*)T) =>
(* 148 *)
match (*S12*)x0 as t1 return
(* 149 *)
((*S8*)sumbool
(*150*) ((*S10*)@eq (*S1*)T (*151*)((*S127*)C2 (*S25*)t (*S26*)t0) (*S12*)t1)
(*152*) ((*S14*)not (*S150*)(@eq T (C2 t t0) t1)))
with
| C1 t1 t2 =>
(* 153 (app) *)
(* 154 *)(fun (t3:(*S1*)T) (*155*) (t4 : (*S1*)T) =>
(* 156 *)
(*S76*)@right
(*157*)((*S10*)@eq (*S1*)T (*158*)((*S127*)C2 (*S34*)t (*S98*)t0) (*159*)((*S24*)C1 (*S11*)t3 (*S12*)t4))
(*160*)((*S14*)not (*S157*)(@eq T (C2 t t0) (C1 t3 t4)))
(* 161 (cast) *)
((*162*)(fun H1 : (*S157*)@eq T (C2 t t0) (C1 t3 t4) =>
(*163*)let H2 : (*S138*)False :=
(* 164 *)
(*S133*)@eq_ind (*S1*)T (*165*)((*S127*)C2 (*S41*)t (*S42*)t0)
(*166*)(fun e : (*S1*)T =>
(*167*)match (*S12*)e return (*S136*)Prop with
| C1 _ _ => (*S138*)False
| C2 _ _ => (*S137*)True
end)
(*S139*)I
(*S43*)(C1 t3 t4)
(*S12*)H1
in
(*S141*)
False_ind False H2)
:
(* S160 *)
not (@eq T (C2 t t0) (C1 t3 t4))))
(*S11*)t1
(*S12*)t2
| C2 t1 t2 =>
(* 168(app) *)
(*169*)(fun (t3:(*S1*)T) (*170*) (t4 : (*S1*)T) =>
(*171*)
(*S32*)@sumbool_rec (*S33*)(@eq T t t3) (*S35*)(not (@eq T t t3))
(*172*)(fun _ : (*S37*) sumbool (@eq T t t3) (not (@eq T t t3)) =>
(*173*)
(*S8*)sumbool
(*174*)((*S10*)@eq (*S1*)T (*S165*)(C2 t t0) (*S140*)(C2 t3 t4))
(*175*)((*S14*)not (*S174*)(@eq T (C2 t t0) (C2 t3 t4))))
(*176*)(fun a : (*S33*)@eq T t t3 =>
(*177*)
(*S32*)@sumbool_rec (*S48*)(@eq T t0 t4) (*S49*)(not (@eq T t0 t4))
(*178*)(fun _ : (*S51*) sumbool (@eq T t0 t4) (not (@eq T t0 t4)) =>
(*179*)
(*S8*)sumbool
(*180*)((*S10*)@eq (*S1*)T
(*181*)((*S127*)C2 (*S55*)t (*S34*)t0)
(*182*)((*S127*)C2 (*S26*)t3 (*S44*)t4))
(*183*) ((*S14*)not (*S180*)(@eq T (C2 t t0) (C2 t3 t4))))
(* 184 *) (fun a0 : (*S48*)@eq T t0 t4 =>
(* 185 *)
(*S60*)@left (*S180*)(@eq T (C2 t t0) (C2 t3 t4))
(*S183*)(not (@eq T (C2 t t0) (C2 t3 t4)))
(*186*)((*S62*)@eq_ind_r (*S1*)T (*S26*)t3
(*187*)(fun t5 : (*S1*)T =>
(*188*)
(*S10*)@eq (*S1*)T
(*189*)((*S127*)C2 (*S12*)t5 (*S41*)t0)
(*190*)((*S127*)C2 (*S67*)t3 (*S26*)t4))
(*191*)((*S62*)@eq_ind_r (*S1*)T (*S44*)t4
(*S192*)(fun t5 : (*S1*)T =>
(*193*)
(*S10*)@eq (*S1*)T
(*194*)((*S127*)C2 (*S67*)t3 (*S12*)t5)
(*S190*)(C2 t3 t4))
(*195*)((*S73*)@eq_refl (*S1*)T (*S182*)(C2 t3 t4))
(*S34*)t0
(*S12*)a0)
(*S55*)t
(*S11*)a))
(*196*)(fun diseq : (*S49*) not (@eq T t0 t4) =>
(*197*)
(*S76*)@right (*S180*)(@eq T (C2 t t0) (C2 t3 t4)) (*183*)(not (@eq T (C2 t t0) (C2 t3 t4)))
(*198*)((*S62*)@eq_ind_r (*S1*)T (*S26*)t3
(*199*)(fun t5 : (*S1*)T =>
(*200*)
(*S14*)not (*S188*)(@eq T (C2 t5 t0) (C2 t3 t4)))
(*201(cast)*)(
(*202*)(fun absurd : (*203*) ((*S10*)@eq) (*S1*)T
(*204*)((*S127*)C2 (*S26*)t3 (*S34*)t0)
(*S182*)(C2 t3 t4) =>
(*205*)
(*S11*)diseq
(*206*)(let H1 : (*S92*) @eq T t0 t4 :=
(* 207 *)
(*S87*)@f_equal (*S1*)T (*S1*)T
(*208*)(fun e : (*S1*)T =>
(*209*)
match (*S12*)e return (*S1*)T with
| C1 _ _ => (*S90*)t0
| C2 _ t5 => (*S12*)t5
end)
(*210*)((*S127*)C2 (*S67*)t3 (*S41*)t0)
(*S190*)(C2 t3 t4)
(*S12*)absurd
in
(* S93 (app) *)
(fun H2 : @eq T t0 t4 => H2)
H1))
:
(* 211 *)
(*S14*)not (*S203*)(@eq T (C2 t3 t0) (C2 t3 t4)))
(*S55*)t
(*S11*)a))
(*S97*)(H0 t4))
(*212*)(fun diseq : (*S35*) not (@eq T t t3) =>
(*213*)
(*S76*)@right
(*S174*)(@eq T (C2 t t0) (C2 t3 t4))
(*S175*)(not (@eq T (C2 t t0) (C2 t3 t4)))
(*214(cast)*)((*215*)(fun absurd : (*S174*) @eq T (C2 t t0) (C2 t3 t4) =>
(*216*)
(*S11*)diseq
(*217*)(let H1 : (*S109*) @eq T t t3 :=
(* 218 *)
(*S87*)@f_equal (*S1*)T (*S1*)T
(*219*)(fun e : (*S1*)T =>
(*220*)
match (*S12*)e return (*S1*)T with
| C1 _ _ => (*S108*)t
| C2 t5 _ => (*S11*)t5
end)
(*S181*)(C2 t t0)
(*S182*)(C2 t3 t4)
(*S12*)absurd
in
(* 221(app) *)
((*222*)let H2 : (* S92 *) @eq T t0 t4 :=
(*223*)
(*S87*)@f_equal (*S1*)T (*S1*)T
(*S208*)(fun e : T =>
match e return T with
| C1 _ _ => t0
| C2 _ t5 => t5
end)
(*S224*)((*S127*)C2 (*S114*)t (*S41*)t0)
(*S190*)(C2 t3 t4)
(*S11*)absurd
in
(*S115(app)*)
(fun (_ : @eq T t0 t4) (H3 : @eq T t t3) => H3)
H2)
(*S12*) H1))
:
(* S175 *)
not (@eq T (C2 t t0) (C2 t3 t4))))
(*S119*)(H t3))
(*S11*)t1
(*S12*)t2
end)
(*S11*)x
(*S12*)y)
Raw
03raw sharing info
Fresh 0,
Fresh 1,
Fresh 2,
Seen 1,
Fresh 3,
Fresh 4,
Fresh 5,
Seen 1,
Fresh 6,
Seen 1,
Fresh 7,
Fresh 8,
Fresh 9,
Fresh 10,
Seen 1,
Fresh 11,
Fresh 12,
Fresh 13,
Fresh 14,
Seen 9,
Fresh 15,
Seen 1,
Fresh 16,
Seen 6,
Fresh 17,
Seen 1,
Fresh 18,
Seen 6,
Fresh 19,
Seen 1,
Fresh 20,
Fresh 21,
Seen 8,
Fresh 22,
Seen 10,
Seen 1,
Fresh 23,
Fresh 24,
Fresh 25,
Fresh 26,
Seen 12,
Fresh 27,
Seen 14,
Seen 22,
Seen 12,
Fresh 28,
Fresh 29,
Seen 1,
Fresh 30,
Seen 1,
Fresh 31,
Fresh 32,
Fresh 33,
Seen 10,
Seen 1,
Fresh 34,
Seen 11,
Fresh 35,
Seen 14,
Seen 33,
Fresh 36,
Fresh 37,
Seen 8,
Seen 33,
Seen 35,
Fresh 38,
Seen 8,
Fresh 39,
Seen 10,
Seen 1,
Fresh 40,
Seen 24,
Fresh 41,
Fresh 42,
Fresh 43,
Seen 24,
Fresh 44,
Seen 11,
Fresh 45,
Seen 14,
Seen 39,
Fresh 46,
Seen 33,
Fresh 47,
Seen 32,
Fresh 48,
Seen 10,
Seen 1,
Seen 42,
Seen 11,
Fresh 49,
Seen 14,
Seen 48,
Fresh 50,
Fresh 51,
Seen 8,
Seen 48,
Seen 49,
Fresh 52,
Seen 8,
Fresh 53,
Seen 10,
Seen 1,
Fresh 54,
Seen 24,
Fresh 55,
Seen 34,
Fresh 56,
Seen 24,
Seen 26,
Seen 44,
Fresh 57,
Seen 14,
Seen 53,
Fresh 58,
Seen 48,
Fresh 59,
Fresh 60,
Seen 53,
Seen 57,
Fresh 61,
Fresh 62,
Seen 1,
Seen 26,
Fresh 63,
Seen 1,
Fresh 64,
Seen 10,
Seen 1,
Fresh 65,
Seen 24,
Seen 12,
Seen 41,
Fresh 66,
Seen 24,
Fresh 67,
Seen 26,
Fresh 68,
Seen 62,
Seen 1,
Seen 44,
Fresh 69,
Seen 1,
Fresh 70,
Seen 10,
Seen 1,
Fresh 71,
Seen 24,
Seen 67,
Seen 12,
Seen 66,
Fresh 72,
Fresh 73,
Seen 1,
Seen 56,
Seen 34,
Seen 12,
Seen 55,
Seen 11,
Fresh 74,
Seen 49,
Fresh 75,
Fresh 76,
Seen 53,
Seen 57,
Fresh 77,
Seen 62,
Seen 1,
Seen 26,
Fresh 78,
Seen 1,
Fresh 79,
Seen 14,
Seen 64,
Fresh 80,
Fresh 81,
Fresh 82,
Seen 10,
Seen 1,
Fresh 83,
Seen 24,
Seen 26,
Seen 34,
Seen 56,
Fresh 84,
Seen 11,
Fresh 85,
Fresh 86,
Fresh 87,
Seen 1,
Seen 1,
Fresh 88,
Seen 1,
Fresh 89,
Seen 1,
Seen 12,
Seen 12,
Fresh 90,
Fresh 91,
Seen 24,
Seen 67,
Seen 41,
Seen 66,
Seen 12,
Fresh 92,
Seen 10,
Seen 1,
Seen 41,
Seen 26,
Fresh 93,
Fresh 94,
Fresh 95,
Seen 10,
Seen 1,
Seen 55,
Seen 67,
Seen 12,
Seen 12,
Fresh 96,
Seen 14,
Seen 82,
Seen 55,
Seen 11,
Fresh 97,
Fresh 98,
Seen 11,
Fresh 99,
Seen 35,
Fresh 100,
Seen 76,
Seen 39,
Seen 45,
Fresh 101,
Fresh 102,
Seen 39,
Fresh 103,
Seen 11,
Fresh 104,
Fresh 105,
Seen 87,
Seen 1,
Seen 1,
Fresh 106,
Seen 1,
Fresh 107,
Seen 1,
Seen 12,
Seen 11,
Fresh 108,
Seen 54,
Seen 56,
Seen 12,
Fresh 109,
Seen 10,
Seen 1,
Seen 55,
Seen 26,
Fresh 110,
Fresh 111,
Fresh 112,
Seen 87,
Seen 1,
Seen 1,
Seen 88,
Fresh 113,
Seen 24,
Fresh 114,
Seen 41,
Seen 66,
Seen 11,
Seen 92,
Fresh 115,
Fresh 116,
Seen 95,
Fresh 117,
Fresh 118,
Seen 10,
Seen 1,
Seen 108,
Seen 98,
Seen 12,
Seen 12,
Seen 12,
Seen 45,
Fresh 119,
Seen 42,
Seen 11,
Seen 11,
Seen 12,
Fresh 120,
Fresh 121,
Seen 1,
Fresh 122,
Seen 1,
Fresh 123,
Seen 76,
Fresh 124,
Seen 10,
Seen 1,
Fresh 125,
Seen 24,
Seen 34,
Seen 98,
Fresh 126,
Fresh 127,
Seen 11,
Seen 12,
Fresh 128,
Seen 14,
Seen 124,
Fresh 129,
Fresh 130,
Seen 124,
Fresh 131,
Fresh 132,
Fresh 133,
Seen 1,
Seen 40,
Fresh 134,
Seen 1,
Fresh 135,
Fresh 136,
Seen 12,
Fresh 137,
Fresh 138,
Fresh 139,
Fresh 140,
Seen 127,
Seen 44,
Seen 11,
Seen 12,
Seen 138,
Fresh 141,
Fresh 142,
Seen 138,
Seen 12,
Seen 128,
Seen 11,
Seen 12,
Fresh 143,
Seen 1,
Fresh 144,
Seen 6,
Fresh 145,
Seen 1,
Fresh 146,
Seen 6,
Fresh 147,
Seen 1,
Fresh 148,
Fresh 149,
Seen 8,
Fresh 150,
Seen 10,
Seen 1,
Fresh 151,
Seen 127,
Seen 25,
Seen 26,
Seen 12,
Fresh 152,
Seen 14,
Seen 150,
Seen 12,
Fresh 153,
Fresh 154,
Seen 1,
Fresh 155,
Seen 1,
Fresh 156,
Seen 76,
Fresh 157,
Seen 10,
Seen 1,
Fresh 158,
Seen 127,
Seen 34,
Seen 98,
Fresh 159,
Seen 24,
Seen 11,
Seen 12,
Fresh 160,
Seen 14,
Seen 157,
Fresh 161,
Fresh 162,
Seen 157,
Fresh 163,
Fresh 164,
Seen 133,
Seen 1,
Fresh 165,
Seen 127,
Seen 41,
Seen 42,
Fresh 166,
Seen 1,
Fresh 167,
Seen 136,
Seen 12,
Seen 138,
Seen 137,
Seen 139,
Seen 43,
Seen 12,
Seen 138,
Seen 141,
Seen 160,
Seen 11,
Seen 12,
Fresh 168,
Fresh 169,
Seen 1,
Fresh 170,
Seen 1,
Fresh 171,
Seen 32,
Seen 33,
Seen 35,
Fresh 172,
Seen 37,
Fresh 173,
Seen 8,
Fresh 174,
Seen 10,
Seen 1,
Seen 165,
Seen 140,
Fresh 175,
Seen 14,
Seen 174,
Fresh 176,
Seen 33,
Fresh 177,
Seen 32,
Seen 48,
Seen 49,
Fresh 178,
Seen 51,
Fresh 179,
Seen 8,
Fresh 180,
Seen 10,
Seen 1,
Fresh 181,
Seen 127,
Seen 55,
Seen 34,
Fresh 182,
Seen 127,
Seen 26,
Seen 44,
Fresh 183,
Seen 14,
Seen 180,
Fresh 184,
Seen 48,
Fresh 185,
Seen 60,
Seen 180,
Seen 183,
Fresh 186,
Seen 62,
Seen 1,
Seen 26,
Fresh 187,
Seen 1,
Fresh 188,
Seen 10,
Seen 1,
Fresh 189,
Seen 127,
Seen 12,
Seen 41,
Fresh 190,
Seen 127,
Seen 67,
Seen 26,
Fresh 191,
Seen 62,
Seen 1,
Seen 44,
Fresh 192,
Seen 1,
Fresh 193,
Seen 10,
Seen 1,
Fresh 194,
Seen 127,
Seen 67,
Seen 12,
Seen 190,
Fresh 195,
Seen 73,
Seen 1,
Seen 182,
Seen 34,
Seen 12,
Seen 55,
Seen 11,
Fresh 196,
Seen 49,
Fresh 197,
Seen 76,
Seen 180,
Seen 183,
Fresh 198,
Seen 62,
Seen 1,
Seen 26,
Fresh 199,
Seen 1,
Fresh 200,
Seen 14,
Seen 188,
Fresh 201,
Fresh 202,
Fresh 203,
Seen 10,
Seen 1,
Fresh 204,
Seen 127,
Seen 26,
Seen 34,
Seen 182,
Fresh 205,
Seen 11,
Fresh 206,
Fresh 207,
Seen 87,
Seen 1,
Seen 1,
Fresh 208,
Seen 1,
Fresh 209,
Seen 1,
Seen 12,
Seen 90,
Seen 12,
Fresh 210,
Seen 127,
Seen 67,
Seen 41,
Seen 190,
Seen 12,
Seen 92,
Seen 93,
Fresh 211,
Seen 14,
Seen 203,
Seen 55,
Seen 11,
Seen 97,
Fresh 212,
Seen 35,
Fresh 213,
Seen 76,
Seen 174,
Seen 175,
Fresh 214,
Fresh 215,
Seen 174,
Fresh 216,
Seen 11,
Fresh 217,
Fresh 218,
Seen 87,
Seen 1,
Seen 1,
Fresh 219,
Seen 1,
Fresh 220,
Seen 1,
Seen 12,
Seen 108,
Seen 11,
Seen 181,
Seen 182,
Seen 12,
Seen 109,
Fresh 221,
Fresh 222,
Fresh 223,
Seen 87,
Seen 1,
Seen 1,
Seen 208,
Fresh 224,
Seen 127,
Seen 114,
Seen 41,
Seen 190,
Seen 11,
Seen 92,
Seen 115,
Seen 12,
Seen 175,
Seen 119,
Seen 11,
Seen 12,
Seen 11,
Seen 12
Raw
04trace
Fresh 0
Fresh 1
Fresh 2
Seen 1
Fresh 3
Fresh 4
Fresh 5
Fresh 6
Seen 1
Fresh 7
Fresh 8
Fresh 9
Fresh 10
Seen 5
Fresh 0
Fresh 1
Fresh 2
Seen 1
Fresh 3
Fresh 4
Fresh 5
Seen 1
Fresh 6
Seen 1
Fresh 7
Fresh 8
Fresh 9
Fresh 10
Seen 1
Fresh 11
Fresh 12
Fresh 13
Fresh 14
Seen 9
Fresh 15
Seen 1
Fresh 16
Seen 6
Fresh 17
Seen 1
Fresh 18
Seen 6
Fresh 19
Seen 1
Fresh 20
Fresh 21
Seen 8
Fresh 22
Seen 10
Seen 1
Fresh 23
Fresh 24
Fresh 25
Fresh 26
Seen 12
Fresh 27
Seen 14
Seen 22
Seen 12
Fresh 28
Fresh 29
Seen 1
Fresh 30
Seen 1
Fresh 31
Fresh 32
Fresh 33
Seen 10
Seen 1
Fresh 34
Seen 11
Fresh 35
Seen 14
Seen 33
Fresh 36
Fresh 37
Seen 8
Seen 33
Seen 35
Fresh 38
Seen 8
Fresh 39
Seen 10
Seen 1
Fresh 40
Seen 24
Fresh 41
Fresh 42
Fresh 43
Seen 24
Fresh 44
Seen 11
Fresh 45
Seen 14
Seen 39
Fresh 46
Seen 33
Fresh 47
Seen 32
Fresh 48
Seen 10
Seen 1
Seen 42
Seen 11
Fresh 49
Seen 14
Seen 48
Fresh 50
Fresh 51
Seen 8
Seen 48
Seen 49
Fresh 52
Seen 8
Fresh 53
Seen 10
Seen 1
Fresh 54
Seen 24
Fresh 55
Seen 34
Fresh 56
Seen 24
Seen 26
Seen 44
Fresh 57
Seen 14
Seen 53
Fresh 58
Seen 48
Fresh 59
Fresh 60
Seen 53
Seen 57
Fresh 61
Fresh 62
Seen 1
Seen 26
Fresh 63
Seen 1
Fresh 64
Seen 10
Seen 1
Fresh 65
Seen 24
Seen 12
Seen 41
Fresh 66
Seen 24
Fresh 67
Seen 26
Fresh 68
Seen 62
Seen 1
Seen 44
Fresh 69
Seen 1
Fresh 70
Seen 10
Seen 1
Fresh 71
Seen 24
Seen 67
Seen 12
Seen 66
Fresh 72
Fresh 73
Seen 1
Seen 56
Seen 34
Seen 12
RESTART
Seen 55
Seen 11
RESTART
Fresh 74
Seen 49
Fresh 75
Fresh 76
Seen 53
Seen 57
Fresh 77
Seen 62
Seen 1
Seen 26
Fresh 78
Seen 1
Fresh 79
Seen 14
Seen 64
Fresh 80
Fresh 81
Fresh 82
Seen 10
Seen 1
Fresh 83
Seen 24
Seen 26
Seen 34
Seen 56
Fresh 84
Seen 11
RESTART
Fresh 85
Fresh 86
Fresh 87
Seen 1
Seen 1
Fresh 88
Seen 1
Fresh 89
Seen 1
Seen 12
Seen 12
Fresh 90
Fresh 91
Seen 24
Seen 67
Seen 41
Seen 66
Seen 12
RESTART
Fresh 92
Seen 10
Seen 1
Seen 41
Seen 26
Fresh 93
Fresh 94
Fresh 95
Seen 10
Seen 1
Seen 55
Seen 67
Seen 12
RESTART
Seen 12
RESTART
Fresh 96
Seen 14
Seen 82
Seen 55
Seen 11
Fresh 97
Fresh 98
Seen 11
Fresh 99
Seen 35
Fresh 100
Seen 76
Seen 39
Seen 45
Fresh 101
Fresh 102
Seen 39
Fresh 103
Seen 11
RESTART
Fresh 104
Fresh 105
Seen 87
Seen 1
Seen 1
Fresh 106
Seen 1
Fresh 107
Seen 1
Seen 12
Seen 11
Fresh 108
Seen 54
Seen 56
Seen 12
RESTART
Fresh 109
Seen 10
Seen 1
Seen 55
Seen 26
Fresh 110
Fresh 111
Fresh 112
Seen 87
Seen 1
Seen 1
Seen 88
Fresh 113
Seen 24
Fresh 114
Seen 41
Seen 66
Seen 11
RESTART
Seen 92
Fresh 115
Fresh 116
Seen 95
Fresh 117
Fresh 118
Seen 10
Seen 1
Seen 108
Seen 98
RESTART
Seen 12
RESTART
Seen 12
RESTART
Seen 12
RESTART
Seen 45
Fresh 119
Seen 42
RESTART
Seen 11
Seen 11
Seen 12
Fresh 120
Fresh 121
Seen 1
Fresh 122
Seen 1
Fresh 123
Seen 76
Fresh 124
Seen 10
Seen 1
Fresh 125
Seen 24
Seen 34
Seen 98
Fresh 126
Fresh 127
Seen 11
Seen 12
Fresh 128
Seen 14
Seen 124
Fresh 129
Fresh 130
Seen 124
Fresh 131
Fresh 132
Fresh 133
Seen 1
Seen 40
Fresh 134
Seen 1
Fresh 135
Fresh 136
Seen 12
Fresh 137
Fresh 138
Fresh 139
Fresh 140
Seen 127
Seen 44
Seen 11
Seen 12
RESTART
Seen 138
Fresh 141
Fresh 142
Seen 138
Seen 12
RESTART
Seen 128
Seen 11
Seen 12
Fresh 143
Seen 1
Fresh 144
Seen 6
Fresh 145
Seen 1
Fresh 146
Seen 6
Fresh 147
Seen 1
Fresh 148
Fresh 149
Seen 8
Fresh 150
Seen 10
Seen 1
Fresh 151
Seen 127
Seen 25
Seen 26
Seen 12
Fresh 152
Seen 14
Seen 150
Seen 12
Fresh 153
Fresh 154
Seen 1
Fresh 155
Seen 1
Fresh 156
Seen 76
Fresh 157
Seen 10
Seen 1
Fresh 158
Seen 127
Seen 34
Seen 98
Fresh 159
Seen 24
Seen 11
Seen 12
Fresh 160
Seen 14
Seen 157
Fresh 161
Fresh 162
Seen 157
Fresh 163
Fresh 164
Seen 133
Seen 1
Fresh 165
Seen 127
Seen 41
Seen 42
Fresh 166
Seen 1
Fresh 167
Seen 136
Seen 12
Seen 138
Seen 137
Seen 139
Seen 43
Seen 12
RESTART
Seen 138
Seen 141
RESTART
Fresh 142
SKIP
Seen 138
Seen 12
RESTART
Seen 160
Seen 11
Seen 12
Fresh 168
Fresh 169
Seen 1
Fresh 170
Seen 1
Fresh 171
Seen 32
Seen 33
Seen 35
Fresh 172
Seen 37
Fresh 173
Seen 8
Fresh 174
Seen 10
Seen 1
Seen 165
Seen 140
Fresh 175
Seen 14
Seen 174
Fresh 176
Seen 33
Fresh 177
Seen 32
Seen 48
Seen 49
Fresh 178
Seen 51
Fresh 179
Seen 8
Fresh 180
Seen 10
Seen 1
Fresh 181
Seen 127
Seen 55
Seen 34
Fresh 182
Seen 127
Seen 26
Seen 44
Fresh 183
Seen 14
Seen 180
Fresh 184
Seen 48
Fresh 185
Seen 60
Seen 180
Seen 183
Fresh 186
Seen 62
Seen 1
Seen 26
Fresh 187
Seen 1
Fresh 188
Seen 10
Seen 1
Fresh 189
Seen 127
Seen 12
Seen 41
Fresh 190
Seen 127
Seen 67
Seen 26
Fresh 191
Seen 62
Seen 1
Seen 44
Fresh 192
Seen 1
Fresh 193
Seen 10
Seen 1
Fresh 194
Seen 127
Seen 67
Seen 12
Seen 190
Fresh 195
Seen 73
Seen 1
Seen 182
Seen 34
Seen 12
Seen 55
Seen 11
Fresh 196
Seen 49
Fresh 197
Seen 76
Seen 180
Seen 183
Fresh 198
Seen 62
Seen 1
Seen 26
Fresh 199
Seen 1
Fresh 200
Seen 14
Seen 188
Fresh 201
Fresh 202
Fresh 203
Seen 10
Seen 1
Fresh 204
Seen 127
Seen 26
Seen 34
Seen 182
Fresh 205
Seen 11
Fresh 206
Fresh 207
Seen 87
Seen 1
Seen 1
Fresh 208
Seen 1
Fresh 209
Seen 1
Seen 12
Seen 90
Seen 12
Fresh 210
Seen 127
Seen 67
Seen 41
Seen 190
Seen 12
RESTART
Seen 92
Seen 93
RESTART
Fresh 94
SKIP
Seen 12
RESTART
Fresh 211
Seen 14
Seen 203
Seen 55
Seen 11
Seen 97
Fresh 212
Seen 35
Fresh 213
Seen 76
Seen 174
Seen 175
Fresh 214
Fresh 215
Seen 174
Fresh 216
Seen 11
Fresh 217
Fresh 218
Seen 87
Seen 1
Seen 1
Fresh 219
Seen 1
Fresh 220
Seen 1
Seen 12
Seen 108
Seen 11
Seen 181
Seen 182
Seen 12
RESTART
Seen 109
Fresh 221
Fresh 222
Fresh 223
Seen 87
Seen 1
Seen 1
Seen 208
Fresh 224
Seen 127
Seen 114
Seen 41
Seen 190
Seen 11
RESTART
Seen 92
Seen 115
RESTART
Fresh 116
SKIP
Seen 42
Raw
05sharing index ==> term
0 ==> (...)
1 ==> T
2 ==> (...)
3 ==> (...)
4 ==> T_rec
5 ==> (fun x : T => forall x0 : T, sumbool (eq T x x0) (not (eq T x x0)))
6 ==> (forall x0 : T,
sumbool (eq T _UNBOUND_REL_2 x0) (not (eq T _UNBOUND_REL_2 x0)))
7 ==> (sumbool (eq T _UNBOUND_REL_2 _UNBOUND_REL_1)
(not (eq T _UNBOUND_REL_2 _UNBOUND_REL_1)))
8 ==> sumbool
9 ==> (eq T _UNBOUND_REL_2 _UNBOUND_REL_1)
10 ==> eq
11 ==> _UNBOUND_REL_2
12 ==> _UNBOUND_REL_1
13 ==> (not (eq T _UNBOUND_REL_2 _UNBOUND_REL_1))
14 ==> not
15 ==> (...)
16 ==> (...)
17 ==> (...)
18 ==> (...)
19 ==> (...)
20 ==> (...)
21 ==> (sumbool
(eq T (CSTR.T._0._1 _UNBOUND_REL_6 _UNBOUND_REL_4) _UNBOUND_REL_1)
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_6 _UNBOUND_REL_4)
_UNBOUND_REL_1)))
22 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_6 _UNBOUND_REL_4) _UNBOUND_REL_1)
23 ==> (CSTR.T._0._1 _UNBOUND_REL_6 _UNBOUND_REL_4)
24 ==> CSTR.T._0._1
25 ==> _UNBOUND_REL_6
26 ==> _UNBOUND_REL_4
27 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_6 _UNBOUND_REL_4) _UNBOUND_REL_1))
28 ==> (...)
29 ==> (...)
30 ==> (...)
31 ==> (...)
32 ==> sumbool_rec
33 ==> (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)
34 ==> _UNBOUND_REL_9
35 ==> (not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2))
36 ==> (fun
_ : sumbool (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))))
37 ==> (sumbool (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)))
38 ==> (sumbool
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))))
39 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))
40 ==> (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
41 ==> _UNBOUND_REL_10
42 ==> _UNBOUND_REL_8
43 ==> (CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2)
44 ==> _UNBOUND_REL_3
45 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2)))
46 ==> (...)
47 ==> (...)
48 ==> (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
49 ==> (not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2))
50 ==> (fun
_ : sumbool (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))))
51 ==> (sumbool (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)))
52 ==> (sumbool
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))))
53 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
54 ==> (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
55 ==> _UNBOUND_REL_11
56 ==> (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)
57 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
58 ==> (fun a0 : eq T _UNBOUND_REL_8 _UNBOUND_REL_2 =>
CSTR.sumbool._0._1
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._1 _UNBOUND_REL_5 t0)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 a0) _UNBOUND_REL_11 _UNBOUND_REL_2))
59 ==> (CSTR.sumbool._0._1
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._1 _UNBOUND_REL_5 t0)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1) _UNBOUND_REL_11
_UNBOUND_REL_2))
60 ==> CSTR.sumbool._0._1
61 ==> (eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._1 _UNBOUND_REL_5 t0)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1) _UNBOUND_REL_11 _UNBOUND_REL_2)
62 ==> eq_ind_r
63 ==> (fun t : T =>
eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
64 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_1 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
65 ==> (CSTR.T._0._1 _UNBOUND_REL_1 _UNBOUND_REL_10)
66 ==> (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)
67 ==> _UNBOUND_REL_5
68 ==> (eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._1 _UNBOUND_REL_5 t0)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1)
69 ==> (fun t0 : T =>
eq T (CSTR.T._0._1 _UNBOUND_REL_5 t0)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
70 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_1)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4))
71 ==> (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_1)
72 ==> (CSTR.eq._0._1 T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
73 ==> CSTR.eq._0._1
74 ==> (fun diseq : not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
diseq
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2))
75 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2))
76 ==> CSTR.sumbool._0._2
77 ==> (eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2)
78 ==> (fun t : T =>
not
(eq T (CSTR.T._0._1 t _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)))
79 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_1 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)))
80 ==> ((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
81 ==> (fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
82 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3))
83 ==> (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
84 ==> (_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
85 ==> (let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1 in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1)
86 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1)
87 ==> f_equal
88 ==> (fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end)
89 ==> match _UNBOUND_REL_1 return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end
90 ==> _UNBOUND_REL_13
91 ==> (CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_10)
92 ==> (eq T _UNBOUND_REL_10 _UNBOUND_REL_4)
93 ==> ((fun H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H1) _UNBOUND_REL_1)
94 ==> (fun H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H1)
95 ==> (eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
96 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3)))
97 ==> (_UNBOUND_REL_7 _UNBOUND_REL_2)
98 ==> _UNBOUND_REL_7
99 ==> (fun diseq : not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2)))
((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
diseq
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))))
100 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2)))
((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2)
H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2))))
101 ==> ((fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2)))
102 ==> (fun
absurd : eq T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
103 ==> (_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1
in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4)
_UNBOUND_REL_2 in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
104 ==> (let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1 in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2
in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1)
105 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end) (CSTR.T._0._1 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._1 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1)
106 ==> (fun e : T =>
match e return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end)
107 ==> match _UNBOUND_REL_1 return T with
| CSTR.T._0._1 t _ => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_14
end
108 ==> _UNBOUND_REL_14
109 ==> (eq T _UNBOUND_REL_11 _UNBOUND_REL_4)
110 ==> ((let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2
in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2) H1)
_UNBOUND_REL_1)
111 ==> (let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2 in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2) H1)
112 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ t => t
| CSTR.T._0._2 _ _ => _UNBOUND_REL_13
end) (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._1 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2)
113 ==> (CSTR.T._0._1 _UNBOUND_REL_12 _UNBOUND_REL_10)
114 ==> _UNBOUND_REL_12
115 ==> ((fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2)
_UNBOUND_REL_1)
116 ==> (fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2)
117 ==> (fun H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7 => H2)
118 ==> (eq T _UNBOUND_REL_14 _UNBOUND_REL_7)
119 ==> (_UNBOUND_REL_8 _UNBOUND_REL_2)
120 ==> ((fun t t0 : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0)))
((fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1 (CSTR.T._0._2 t t0) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0)))) _UNBOUND_REL_2 _UNBOUND_REL_1)
121 ==> (fun t t0 : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0)))
((fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1 (CSTR.T._0._2 t t0) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 t t0))))
122 ==> (fun t : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 t))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 t)))
((fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 t) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1 (CSTR.T._0._2 _UNBOUND_REL_3 t) H1
in
False_ind False H2)
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 t))))
123 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1))
(not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1)))
((fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1))))
124 ==> (eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1))
125 ==> (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
126 ==> (CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1)
127 ==> CSTR.T._0._2
128 ==> (not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1)))
129 ==> ((fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1)))
130 ==> (fun
H1 : eq T (CSTR.T._0._1 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._2 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
131 ==> (let H2 : False :=
eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) _UNBOUND_REL_1 in
False_ind False H2)
132 ==> (eq_ind T (CSTR.T._0._1 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end) CSTR.True._0._1
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) _UNBOUND_REL_1)
133 ==> eq_ind
134 ==> (fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end)
135 ==> match _UNBOUND_REL_1 return Prop with
| CSTR.T._0._1 _ _ => True
| CSTR.T._0._2 _ _ => False
end
136 ==> Prop
137 ==> True
138 ==> False
139 ==> CSTR.True._0._1
140 ==> (CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2)
141 ==> (False_ind False _UNBOUND_REL_1)
142 ==> False_ind
143 ==> (...)
144 ==> (...)
145 ==> (...)
146 ==> (...)
147 ==> (...)
148 ==> match
_UNBOUND_REL_1 in (@T t)
return
(sumbool (eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4) t)
(not (eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4) t)))
with
| CSTR.T._0._1 t t0 =>
(fun t1 t2 : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t1 t2)))
((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t1 t2) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1 (CSTR.T._0._1 t1 t2) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t1 t2)))) t t0
| CSTR.T._0._2 t t0 =>
(fun t1 t2 : T =>
sumbool_rec (eq T _UNBOUND_REL_9 t1)
(not (eq T _UNBOUND_REL_9 t1))
(fun
_ : sumbool (eq T _UNBOUND_REL_9 t1)
(not (eq T _UNBOUND_REL_9 t1)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2))))
(fun a : eq T _UNBOUND_REL_9 t1 =>
sumbool_rec (eq T _UNBOUND_REL_8 t2)
(not (eq T _UNBOUND_REL_8 t2))
(fun
_ : sumbool (eq T _UNBOUND_REL_8 t2)
(not (eq T _UNBOUND_REL_8 t2)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2))))
(fun a0 : eq T _UNBOUND_REL_8 t2 =>
CSTR.sumbool._0._1
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2)))
(eq_ind_r T t1
(fun t3 : T =>
eq T (CSTR.T._0._2 t3 _UNBOUND_REL_10)
(CSTR.T._0._2 t1 t2))
(eq_ind_r T t2
(fun t3 : T =>
eq T (CSTR.T._0._2 t1 t3) (CSTR.T._0._2 t1 t2))
(CSTR.eq._0._1 T (CSTR.T._0._2 t1 t2))
_UNBOUND_REL_9 a0) _UNBOUND_REL_11 a))
(fun diseq : not (eq T _UNBOUND_REL_8 t2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2)))
(eq_ind_r T t1
(fun t3 : T =>
not
(eq T (CSTR.T._0._2 t3 _UNBOUND_REL_10)
(CSTR.T._0._2 t1 t2)))
((fun
absurd : eq T (CSTR.T._0._2 t1 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2) =>
diseq
(let H1 : eq T _UNBOUND_REL_10 t2 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t3 => t3
end) (CSTR.T._0._2 t1 _UNBOUND_REL_10)
(CSTR.T._0._2 t1 t2) absurd in
(fun H2 : eq T _UNBOUND_REL_11 t2 => H2) H1))
:
not
(eq T (CSTR.T._0._2 t1 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2))) _UNBOUND_REL_11 a))
(_UNBOUND_REL_7 t2))
(fun diseq : not (eq T _UNBOUND_REL_9 t1) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2)))
((fun
absurd : eq T
(CSTR.T._0._2 _UNBOUND_REL_10
_UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2) =>
diseq
(let H1 : eq T _UNBOUND_REL_11 t1 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t3 _ => t3
end)
(CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 t1 t2) absurd in
(let H2 : eq T _UNBOUND_REL_10 t2 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t3 => t3
end)
(CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 t1 t2) absurd in
(fun (_ : eq T _UNBOUND_REL_11 t2)
(H3 : eq T _UNBOUND_REL_14 t1) => H3) H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 t1 t2)))) (_UNBOUND_REL_8 t1)) t t0
end
149 ==> (sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4)
_UNBOUND_REL_1)
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4)
_UNBOUND_REL_1)))
150 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4) _UNBOUND_REL_1)
151 ==> (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4)
152 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_6 _UNBOUND_REL_4)
_UNBOUND_REL_1))
153 ==> ((fun t t0 : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0)))
((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1 (CSTR.T._0._1 t t0) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0)))) _UNBOUND_REL_2 _UNBOUND_REL_1)
154 ==> (fun t t0 : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0)))
((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1 (CSTR.T._0._1 t t0) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 t t0))))
155 ==> (fun t : T =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 t))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 t)))
((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 t) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1 (CSTR.T._0._1 _UNBOUND_REL_3 t) H1
in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 t))))
156 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1)))
((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1))))
157 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1))
158 ==> (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
159 ==> (CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1)
160 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1)))
161 ==> ((fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1)))
162 ==> (fun
H1 : eq T (CSTR.T._0._2 _UNBOUND_REL_9 _UNBOUND_REL_7)
(CSTR.T._0._1 _UNBOUND_REL_2 _UNBOUND_REL_1) =>
let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) H1 in
False_ind False H2)
163 ==> (let H2 : False :=
eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) _UNBOUND_REL_1 in
False_ind False H2)
164 ==> (eq_ind T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end) CSTR.True._0._1
(CSTR.T._0._1 _UNBOUND_REL_3 _UNBOUND_REL_2) _UNBOUND_REL_1)
165 ==> (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
166 ==> (fun e : T =>
match e return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end)
167 ==> match _UNBOUND_REL_1 return Prop with
| CSTR.T._0._1 _ _ => False
| CSTR.T._0._2 _ _ => True
end
168 ==> (...)
169 ==> (...)
170 ==> (...)
171 ==> (...)
172 ==> (fun
_ : sumbool (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))))
173 ==> (sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))))
174 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))
175 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2)))
176 ==> (fun a : eq T _UNBOUND_REL_9 _UNBOUND_REL_2 =>
sumbool_rec (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2))
(fun
_ : sumbool (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))))
(fun a0 : eq T _UNBOUND_REL_8 _UNBOUND_REL_2 =>
CSTR.sumbool._0._1
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 a0) _UNBOUND_REL_11 a))
(fun diseq : not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)
=>
diseq
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)
absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2)
H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 a)) (_UNBOUND_REL_7 _UNBOUND_REL_2))
177 ==> (sumbool_rec (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2))
(fun
_ : sumbool (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))))
(fun a0 : eq T _UNBOUND_REL_8 _UNBOUND_REL_2 =>
CSTR.sumbool._0._1
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 a0) _UNBOUND_REL_11 _UNBOUND_REL_2))
(fun diseq : not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)
=>
diseq
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)
absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2)
H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2))
(_UNBOUND_REL_7 _UNBOUND_REL_2))
178 ==> (fun
_ : sumbool (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)
(not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2)) =>
sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))))
179 ==> (sumbool
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))))
180 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
181 ==> (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
182 ==> (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)
183 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
184 ==> (fun a0 : eq T _UNBOUND_REL_8 _UNBOUND_REL_2 =>
CSTR.sumbool._0._1
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 a0) _UNBOUND_REL_11 _UNBOUND_REL_2))
185 ==> (CSTR.sumbool._0._1
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1) _UNBOUND_REL_11
_UNBOUND_REL_2))
186 ==> (eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1) _UNBOUND_REL_11 _UNBOUND_REL_2)
187 ==> (fun t : T =>
eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
188 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_1 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
189 ==> (CSTR.T._0._2 _UNBOUND_REL_1 _UNBOUND_REL_10)
190 ==> (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)
191 ==> (eq_ind_r T _UNBOUND_REL_3
(fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
(CSTR.eq._0._1 T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
_UNBOUND_REL_9 _UNBOUND_REL_1)
192 ==> (fun t0 : T =>
eq T (CSTR.T._0._2 _UNBOUND_REL_5 t0)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
193 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_1)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4))
194 ==> (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_1)
195 ==> (CSTR.eq._0._1 T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
196 ==> (fun diseq : not (eq T _UNBOUND_REL_8 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)
=>
diseq
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2))
197 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
(eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)
=>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2))
198 ==> (eq_ind_r T _UNBOUND_REL_4
(fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
((fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
_UNBOUND_REL_11 _UNBOUND_REL_2)
199 ==> (fun t : T =>
not
(eq T (CSTR.T._0._2 t _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
200 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_1 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)))
201 ==> ((fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
202 ==> (fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
203 ==> (eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3))
204 ==> (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
205 ==> (_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1
in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1))
206 ==> (let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1 in
(fun H2 : eq T _UNBOUND_REL_11 _UNBOUND_REL_5 => H2) H1)
207 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_1)
208 ==> (fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end)
209 ==> match _UNBOUND_REL_1 return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end
210 ==> (CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_10)
211 ==> (not
(eq T (CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3)))
212 ==> (fun diseq : not (eq T _UNBOUND_REL_9 _UNBOUND_REL_2) =>
CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2)))
((fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
diseq
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2)
H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))))
213 ==> (CSTR.sumbool._0._2
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))
(not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2)))
((fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2)
H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2))))
214 ==> ((fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
:
not
(eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2)))
215 ==> (fun
absurd : eq T (CSTR.T._0._2 _UNBOUND_REL_10 _UNBOUND_REL_8)
(CSTR.T._0._2 _UNBOUND_REL_3 _UNBOUND_REL_2) =>
_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) absurd in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) absurd in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
216 ==> (_UNBOUND_REL_2
(let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1
in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4)
_UNBOUND_REL_2 in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1))
217 ==> (let H1 : eq T _UNBOUND_REL_11 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1 in
(let H2 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2
in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H3 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H3) H2) H1)
218 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end) (CSTR.T._0._2 _UNBOUND_REL_11 _UNBOUND_REL_9)
(CSTR.T._0._2 _UNBOUND_REL_4 _UNBOUND_REL_3) _UNBOUND_REL_1)
219 ==> (fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end)
220 ==> match _UNBOUND_REL_1 return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_14
| CSTR.T._0._2 t _ => t
end
221 ==> ((let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2
in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2) H1)
_UNBOUND_REL_1)
222 ==> (let H1 : eq T _UNBOUND_REL_10 _UNBOUND_REL_4 :=
f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2 in
(fun (_ : eq T _UNBOUND_REL_11 _UNBOUND_REL_5)
(H2 : eq T _UNBOUND_REL_14 _UNBOUND_REL_7) => H2) H1)
223 ==> (f_equal T T
(fun e : T =>
match e return T with
| CSTR.T._0._1 _ _ => _UNBOUND_REL_13
| CSTR.T._0._2 _ t => t
end) (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
(CSTR.T._0._2 _UNBOUND_REL_5 _UNBOUND_REL_4) _UNBOUND_REL_2)
224 ==> (CSTR.T._0._2 _UNBOUND_REL_12 _UNBOUND_REL_10)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment