Skip to content

Instantly share code, notes, and snippets.

@SkySkimmer

SkySkimmer/sig.txt

Created October 24, 2017 21:26
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save SkySkimmer/771c9b69eda5f7b2c90d7b308470cc53 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save SkySkimmer/771c9b69eda5f7b2c90d7b308470cc53 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
sig.txt
sigma: Evd.evar_map = UNDEFINED EVARS: (+level 2 closure):
?X4==[ |- Type@{test.2}] (internal placeholder) {?T}
?X5==[ |- ?X4] (goal evar) {?Goal}
?X45==[
|- sig
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(fun
to_sigma : forall _ : mix,
sigT
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) =>
forall
v : sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat),
eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)) to_sigma
((fun
ab : sigT
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) =>
CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) ab)) v)) v)
=> CSTR.sig._0._1
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(fun
x : forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat) =>
forall
x0 : sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) => nat),
eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)) x
((fun
ab : sigT
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) =>
CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) ab)) x0)) x0) ?X50
(fun
v : sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat) =>
?X61@{__:=v}
:
eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)) ?X50
((fun
ab : sigT
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) =>
CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) ab))
(projT2
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) ab)) v)) v)] (goal evar)
?X61==[v
|- eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v : mix =>
(fun (a0 : Prop) (b0 : forall _ : nat, a0) (c0 : nat) =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=a0; __:=b0; __:=c0}
?X82@{__:=a0; __:=b0; __:=c0})
?X76@{__:=a0; __:=b0; __:=c0})
(a v) (b v) (c v))
((fun
ab : sigT
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) =>
CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) ab))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) ab))
(projT2
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) => nat)
ab)) v)) v => ?X83@{__:=v}] (goal evar)
?X69==[a0 b0
|- forall _ : nat,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) => nat)
=> fun c0 : nat => ?X70@{__:=a0; __:=b0; __:=c0}] (goal evar)
?X70==[a0 b0 c0
|- sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) => nat)
=> CSTR.sigT._0._1 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) => nat)
?X75@{__:=a0; __:=b0; __:=c0} ?X76@{__:=a0; __:=b0; __:=c0}]
(goal evar)
?X74==[a0 b0 c0 |- ?X71@{__:=a0; __:=b0; __:=c0}
=> ?X75@{__:=a0; __:=b0; __:=c0}] (underscore)
?X75==[a0 b0 c0 |- ?X71@{__:=a0; __:=b0; __:=c0}
=> CSTR.sigT._0._1 Prop (fun a : Prop => forall _ : nat, a)
?X81@{__:=a0; __:=b0; __:=c0} ?X82@{__:=a0; __:=b0; __:=c0}]
(instance of x)
?X76==[a0 b0 c0
|- ?X73@{__:=a0; __:=b0; __:=c0} ?X75@{__:=a0; __:=b0; __:=c0}]
(goal evar) {?Goal0}
?X80==[a0 b0 c0 |- ?X77@{__:=a0; __:=b0; __:=c0}
=> ?X81@{__:=a0; __:=b0; __:=c0}] (underscore)
?X81==[a0 b0 c0 |- ?X77@{__:=a0; __:=b0; __:=c0}] (instance of x) {?x}
?X82==[a0 b0 c0
|- ?X79@{__:=a0; __:=b0; __:=c0} ?X81@{__:=a0; __:=b0; __:=c0}]
(goal evar) {?Goal1}
?X83==[v
|- eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v}
?X82@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v})
?X76@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v))
(projT2 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat) v))) v => ?X84@{__:=v}] (goal evar)
?X84==[v
|- eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v}
?X82@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v})
?X76@{__:=_UNBOUND_REL_3; __:=_UNBOUND_REL_2; __:=v})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v))
(projT2 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat) v))) v
=> match
v as s
return
(eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat))
(fun v : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_3; __:=s; __:=v}
?X82@{__:=_UNBOUND_REL_3; __:=s; __:=v})
?X76@{__:=_UNBOUND_REL_3; __:=s; __:=v})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) s))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) s))
(projT2
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) s))) s)
with
| CSTR.sigT._0._1 x x0 => ?X85@{__:=v} x x0
end] (goal evar)
?X86==[
|- forall (x : sigT Prop (fun a : Prop => forall _ : nat, a))
(n : nat),
eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_4;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) x n;
__:=v}
?X82@{__:=_UNBOUND_REL_4;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) x n;
__:=v})
?X76@{__:=_UNBOUND_REL_4;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) x n; __:=v})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) x n)))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) x n)))
(projT2 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) x n))))
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat) x n)
=> fun v : sigT Prop (fun a : Prop => forall _ : nat, a) =>
?X87@{__:=v}] (goal evar)
?X87==[v
|- forall n : nat,
eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v0 : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_3;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) v n;
__:=v0}
?X82@{__:=_UNBOUND_REL_3;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) v n;
__:=v0})
?X76@{__:=_UNBOUND_REL_3;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v n; __:=v0})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v n)))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v n)))
(projT2 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v n))))
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat) v n) => fun x : nat => ?X88@{__:=v; __:=x}]
(goal evar)
?X88==[v x
|- eq
(sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat))
(id
(forall _ : mix,
sigT (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat))
(fun v0 : mix =>
CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1 Prop
(fun a : Prop => forall _ : nat, a)
?X81@{__:=_UNBOUND_REL_2;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) v x;
__:=v0}
?X82@{__:=_UNBOUND_REL_2;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop =>
forall _ : nat, a) => nat) v x;
__:=v0})
?X76@{__:=_UNBOUND_REL_2;
__:=CSTR.sigT._0._1
(sigT Prop
(fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v x; __:=v0})
(CSTR.mix._0._1
(projT1 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v x)))
(projT2 Prop (fun a : Prop => forall _ : nat, a)
(projT1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a)
=> nat) v x)))
(projT2 (sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop (fun a : Prop => forall _ : nat, a)
=> nat)
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun
_ : sigT Prop
(fun a : Prop => forall _ : nat, a) =>
nat) v x))))
(CSTR.sigT._0._1
(sigT Prop (fun a : Prop => forall _ : nat, a))
(fun _ : sigT Prop (fun a : Prop => forall _ : nat, a) =>
nat) v x)] (goal evar) {?Goal2}
UNIVERSES:
{test.15 test.13 test.12 test.11 test.10 test.9 test.8 test.7 test.6 test.5 test.4 test.3 test.2} |= Set < test.3
Set < test.4
Set < test.6
Set < test.8
Set < test.9
Set < test.10
Set < test.12
Set < test.13
Set < test.15
Prop <= test.6
Prop <= test.10
Prop <= test.13
Prop <= Coq.Init.Specif.8
Prop <= Coq.Init.Specif.23
Set <= Coq.Init.Specif.8
Set <= Coq.Init.Specif.23
test.5 <= Coq.Init.Specif.1
test.5 <= Coq.Init.Datatypes.83
test.6 <= test.5
test.7 <= test.5
test.8 <= test.7
test.8 <= Coq.Init.Logic.8
test.10 <= Coq.Init.Datatypes.83
test.11 <= Coq.Init.Datatypes.83
test.12 <= test.11
test.12 <= Coq.Init.Logic.8
ALGEBRAIC UNIVERSES:
{test.15 test.12 test.11 test.10 test.9 test.8 test.7 test.6 test.5 test.4 test.3 test.2}
UNDEFINED UNIVERSES:
test.15
test.13
test.12
test.11
test.10
test.9
test.8
test.7
test.6
test.5
test.4
test.3
test.2
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment