t_rect = 
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
fix F (t : t) : P t :=
  match t as t0 return (P t0) with
  | k _ x0 => f x0 (F x0)
  end
     : forall P : t -> Type,
       (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t

Argument scopes are [function_scope function_scope _]
     = fun d : TT => match d with
                     | {| f3 := b |} => b
                     end
     : TT -> 0 = 0
     = fun d : TT => match d with
                     | {| f3 := b |} => b
                     end
     : TT -> 0 = 0
proj = 
fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
match Nat.eq_dec x y with
| left eqprf => match eqprf in (_ = z) return (P z) with
                | eq_refl => def
                end
| right _ => prf
end
     : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y

Argument scopes are [nat_scope nat_scope function_scope _ _]
foo = 
fix foo (A : Type) (l : list A) {struct l} : option A :=
  match l with
  | nil => None
  | x0 :: nil => Some x0
  | x0 :: (_ :: _) as l0 => foo A l0
  end
     : forall A : Type, list A -> option A

Argument scopes are [type_scope list_scope]
uncast = 
fun (A : Type) (x : I A) => match x with
                            | x0 <: _ => x0
                            end
     : forall A : Type, I A -> A

Argument scopes are [type_scope _]
foo' = if A 0 then true else false
     : bool
f = 
fun H : B =>
match H with
| AC x =>
    let b0 := b in
    (if b0 as b return (P b -> True)
     then fun _ : P true => Logic.I
     else fun _ : P false => Logic.I) x
end
     : B -> True
The command has indeed failed with message:
Non exhaustive pattern-matching: no clause found for pattern 
gadtTy _ _
The command has indeed failed with message:
In environment
texpDenote : forall t : type, texp t -> typeDenote t
t : type
e : texp t
t1 : type
t2 : type
t0 : type
b : tbinop t1 t2 t0
e1 : texp t1
e2 : texp t2
The term "0" has type "nat" while it is expected to have type
 "typeDenote t0".
fun '{{n, m, _}} => n + m
     : J -> nat
fun '{{n, m, p}} => n + m + p
     : J -> nat
fun '(D n m p q) => n + m + p + q
     : J -> nat
The command has indeed failed with message:
The constructor D (in type J) expects 3 arguments.
lem1 = 
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
     : forall k : nat * nat, k = k
lem2 = 
fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
     : forall k : bool, k = k

Argument scope is [bool_scope]
lem3 = 
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
     : forall k : nat * nat, k = k
1 subgoal
  
  x : nat
  n, n0 := match x + 0 with
           | 0 | S _ => 0
           end : nat
  e,
  e0 := match x + 0 as y return (y = y) with
        | 0 => eq_refl
        | S n => eq_refl
        end : x + 0 = x + 0
  n1, n2 := match x with
            | 0 | S _ => 0
            end : nat
  e1, e2 := match x return (x = x) with
            | 0 => eq_refl
            | S n => eq_refl
            end : x = x
  ============================
  x + 0 = 0
1 subgoal
  
  p : nat
  a,
  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
        | eq_refl => conj eq_refl eq_refl
        end : eq_refl = eq_refl /\ p = p
  a1,
  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
        | eq_refl => conj eq_refl eq_refl
        end : p = p /\ p = p
  ============================
  eq_refl = eq_refl
fun x : comparison => match x with
                      | Eq => 1
                      | _ => 0
                      end
     : comparison -> nat
fun x : comparison => match x with
                      | Eq => 1
                      | Lt => 0
                      | Gt => 0
                      end
     : comparison -> nat
fun x : comparison => match x with
                      | Eq => 1
                      | Lt | Gt => 0
                      end
     : comparison -> nat
fun x : comparison =>
match x return nat with
| Eq => S O
| Lt => O
| Gt => O
end
     : forall _ : comparison, nat
fun x : K => match x with
             | a3 | a4 => 3
             | _ => 2
             end
     : K -> nat
fun x : K => match x with
             | a1 | a2 => 4
             | a3 => 3
             | _ => 2
             end
     : K -> nat
fun x : K => match x with
             | a1 | a2 => 4
             | a4 => 3
             | _ => 2
             end
     : K -> nat
fun x : K => match x with
             | a1 | a3 | a4 => 3
             | _ => 2
             end
     : K -> nat
The command has indeed failed with message:
Pattern "S _, _" is redundant in this clause.