Fix subshape definitions

[fizruk]

This fixes the following bug (missing tope checks):

#lang rzk-1

#define Δ²
  : (2 × 2) → TOPE
  := \ (t, s) → (s ≤ t)

#define Λ
  : Δ² → TOPE
  := \ (t, s) → (s ≡ 0₂) ∨ (t ≡ 1₂)

#define Λ-is-in-Δ²
  (A : U)
  : (Δ² → A) → (Λ → A)
  := \ f t → f t

#define wrong-Λ
  : Δ² → TOPE
  := \ (t, s) → t ≤ s

#define Λ-alt
  : (2 × 2) → TOPE
  := \ (t, s) → (t ≡ 0₂) ∨ (s ≡ 1₂)

#define Λ-alt-is-in-wrong-Λ
  (A : U)
  : (wrong-Λ → A) → (Λ-alt → A)   -- used to be fine before this PR
  -- : (( st : (2 × 2) | wrong-Λ st ) → A) → (Λ-alt → A) -- correctly issued a type error
  := \ f t → f t