gebner / trepplein Goto Github PK

9 #NS 0 u
2 #NS 0 eq
3 #NS 0 alpha
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
5 #NS 0 alpt
2 #EV 1
3 #ES 0
4 #EP #BD 5 2 3
5 #EP #BD 4 1 4
6 #EP #BI 3 0 5
6 #NS 2 refl
7 #EC 2 1
8 #EA 7 2
9 #EA 8 1
10 #EA 9 1
11 #EP #BD 4 1 10
12 #EP #BI 3 0 11
#IND 2 2 6 1 6 12 1

line 4: _Map_base::at

-- successfully checked 3 declarations

9 #NS 0 u = `u
2 #NS 0 eq = `eq
3 #NS 0 alpha = `alpha
1 #UP 1 = u1 (???)
0 #ES 1 = Sort u1
4 #NS 0 a = `a
1 #EV 0 = #0
5 #NS 0 alpt = `alpt
2 #EV 1 = #1
3 #ES 0 = Sort 0
4 #EP #BD 5 2 3 = Π (alpt : #1), Sort 0
5 #EP #BD 4 1 4 = Π (a : #0) (alpt : #0), Sort 0
6 #EP #BI 3 0 5 = Π {alpha : Sort u1} (a : alpha) (alpt : alpha), Sort 0
6 #NS 2 refl = `refl
7 #EC 2 1 = eq.{u1}
8 #EA 7 2 = eq.{u1} #1
9 #EA 8 1 = eq.{u1} #1 #0
10 #EA 9 1 = eq.{u1} #1 #0 #0
11 #EP #BD 4 1 10 = Π (a : #0), eq.{u1} #0 a a
12 #EP #BI 3 0 11 = Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a
#IND 2 2 6 1 6 12 1 =
  inductive {u1} eq {alpha : Sort u1} (a : alpha) : Π (alpt : alpha), Sort 0
  | refl : Π {alpha : Sort u1} (a : alpha), eq.{u1} alpha a a