Skip to content

Instantly share code, notes, and snippets.

@greenrd greenrd/gist:334374
Created Mar 16, 2010

What would you like to do?
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".
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.