gistfile1.txt

Error:
In environment
n : nat
A : TupleT n
B : TupleT n
tm2 : TupleMap n A B
The term
 "(fun (P : forall (n : nat) (T U : TupleT n), TupleMap n T U -> Type)
     (z : P 0 nilT nilT tmNil)
     (s : forall (n : nat) (A B : Type) (F : A -> TupleT n)
            (G : B -> TupleT n)
            (s : forall x : A, sigT (TupleMap n (F x) ∘ G)),
          (forall x : A, P n (F x) (G (projT1 (s x))) (projT2 (s x))) ->
          P (S n) (consT A F) (consT B G) (tmCons F G s)) =>
   TupleMap_superrect P z s n A B tm2) ?566 ?567" has type
 "(forall (n0 : nat) (A0 B0 : Type) (F : A0 -> TupleT n0)
     (G : B0 -> TupleT n0) (s : forall x : A0, sigT (TupleMap n0 (F x) ∘ G)),
   (forall x : A0, ?566 n0 (F x) (G (projT1 (s x))) (projT2 (s x))) ->
   ?566 (S n0) (consT A0 F) (consT B0 G) (tmCons F G s)) -> 
  ?566 n A B tm2" while it is expected to have type
 "(fun (n : nat) (A B : TupleT n) (_ : TupleMap n A B) =>
   forall C : TupleT n, TupleMap n B C -> block (block (TupleMap n A C))) n A
    B tm2".