anchor.diff:               "s PCROSS t = {pastecart (x:A^M) (y:A^N) | x IN s /\ y IN t}")
   
   let FORALL_IN_PCROSS = prove((parse_term "(!z. z IN s PCROSS t ==> P z) <=>
  -   (!x y. x IN s /\ y IN t ==> P(pastecart x y))"),
  -   REWRITE_TAC [PCROSS; FORALL_IN_GSPEC])
  +   (!x y. x IN s /\ y IN t ==> P(pastecart x y))"), REWRITE_TAC [PCROSS; FORALL_IN_GSPEC])
   let EXISTS_IN_PCROSS = prove((parse_term "(?z. z IN s PCROSS t /\ P z) <=>
  -   (?x y. x IN s /\ y IN t /\ P(pastecart x y))"),
  -   REWRITE_TAC [PCROSS; EXISTS_IN_GSPEC; CONJ_ASSOC])
  +   (?x y. x IN s /\ y IN t /\ P(pastecart x y))"), REWRITE_TAC [PCROSS; EXISTS_IN_GSPEC; CONJ_ASSOC])
   let PASTECART_IN_PCROSS = 
       prove
           ((parse_term 
  
positive.code: 
  let LAMBDA_UNIQUE = prove((parse_term "!f:A^B g.
          (!i. 1 <= i /\ i <= dimindex(:B) ==> (f$i = g i)) <=>
          ((lambda) g = f)"),
          SIMP_TAC [CART_EQ; LAMBDA_BETA]
          |> THEN <| MESON_TAC [])
  let LAMBDA_ETA = 
      prove
  
negative.code: 
  let CART_EQ = 
      prove((parse_term "!x:A^B y.
      (x = y) <=> !i. 1 <= i /\ i <= dimindex(:B) ==> (x$i = y$i)"), REPEAT GEN_TAC
      |> THEN <| REWRITE_TAC [finite_index
                              GSYM FORALL_FINITE_INDEX]
      |> THEN <| REWRITE_TAC [GSYM FUN_EQ_THM
  