p 0 0 true
     : 0 = 0 /\ true = true
p 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
p 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
p 0 0
     : forall b : bool, 0 = 0 /\ b = b
p 0 0
     : forall b : bool, 0 = 0 /\ b = b
p
     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p
     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
@p nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
@p
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
p 0 0
     : forall b : bool, 0 = 0 /\ b = b
p
     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p 0 0 true
     : 0 = 0 /\ true = true
p 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
p 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
p 0 0
     : forall b : bool, 0 = 0 /\ b = b
p 0 0
     : forall b : bool, 0 = 0 /\ b = b
p
     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
p
     : forall (a1 a2 : nat) (B : Type) (b : B), a1 = a2 /\ b = b
@p nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
@p
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
f x true
     : 0 = 0 /\ true = true
f x
     : forall b : bool, 0 = 0 /\ b = b
f x
     : forall b : bool, 0 = 0 /\ b = b
@f nat
     : forall a1 a2 : nat,
       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
     : forall (A : Type) (a1 a2 : A),
       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
x.(f) true
     : 0 = 0 /\ true = true
x.(f)
     : forall b : bool, 0 = 0 /\ b = b
x.(f)
     : forall b : bool, 0 = 0 /\ b = b
@f nat
     : forall a1 a2 : nat,
       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
@f
     : forall (A : Type) (a1 a2 : A),
       T a1 a2 -> forall (B : Type) (b : B), a1 = a2 /\ b = b
f
     : T 0 0 -> forall (B : Type) (b : B), 0 = 0 /\ b = b
u ?A
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u ?A
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u nat 0 0 ?B
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
u nat 0 0 bool
     : forall b : bool, 0 = 0 /\ b = b
u nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
u nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
u
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
@u
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
@u
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
u
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
u 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
u 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
@u nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
@u nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
u 0 0 true
     : 0 = 0 /\ true = true
u 0 0 true
     : 0 = 0 /\ true = true
v
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
v 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0 true
     : 0 = 0 /\ true = true
v
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@v 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
@v 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
v 0
     : forall b : bool, 0 = 0 /\ b = b
     = ?n@{x:=v 0 (B:=bool)}
     : nat
v
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
v 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
v 0 true
     : 0 = 0 /\ true = true
v
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
@v 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
@v 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
v 0
     : forall b : bool, 0 = 0 /\ b = b
     = ?n@{x:=v 0 (B:=bool)}
     : nat
##
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
##
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0 true
     : 0 = 0 /\ true = true
## 0 0 true
     : 0 = 0 /\ true = true
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
     = ?n@{x:=## 0 0 (B:=bool)}
     : nat
## ?A
     : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
where
?A : [ |- Type]
##
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
##
     : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
## nat 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## nat 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## nat 0 0
     : forall (B : Type) (b : B), 0 = 0 /\ b = b
## nat 0 0 ?B
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## nat 0 0 ?B
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## nat 0 0 bool
     : forall b : bool, 0 = 0 /\ b = b
## nat 0 0 bool true
     : 0 = 0 /\ true = true
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
     = ?n@{x:=## 0 0 (B:=bool)}
     : nat
## 0 0 true
     : 0 = 0 /\ true = true
## 0 0 true
     : 0 = 0 /\ true = true
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0
     : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b
## 0 0
     : forall b : ?B, 0 = 0 /\ b = b
where
?B : [ |- Type]
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
## 0 0
     : forall b : bool, 0 = 0 /\ b = b
     = ?n@{x:=## 0 0 (B:=bool)}
     : nat
## 0 0 true
     : 0 = 0 /\ true = true
## 0 0 true
     : 0 = 0 /\ true = true
# 0 0 bool 0%bool
     : T
fun a : T => match a with
             | # 0 0 _ _ => 1
             | _ => 2
             end
     : T -> nat
#' 0 0 0%bool
     : T
fun a : T => match a with
             | #' 0 0 _ => 1
             | _ => 2
             end
     : T -> nat
## 0 0 0%bool
     : T
fun a : T => match a with
             | ## 0 0 _ => 1
             | _ => 2
             end
     : T -> nat
##' 0 0 0%bool
     : T
fun a : T => match a with
             | ##' 0 0 _ => 1
             | _ => 2
             end
     : T -> nat
P 0 0 bool 0%bool
     : T
fun a : T => match a with
             | P 0 0 _ _ => 1
             | _ => 2
             end
     : T -> nat
P' 0 0 0%bool
     : T
fun a : T => match a with
             | P' 0 0 _ => 1
             | _ => 2
             end
     : T -> nat
Q 0 0 0%bool
     : T
fun a : T => match a with
             | Q 0 0 _ => 1
             | _ => 2
             end
     : T -> nat
Q' 0 0 0%bool
     : T
fun a : T => match a with
             | Q' 0 0 _ => 1
             | _ => 2
             end
     : T -> nat