`some` in context schema as requirement for instantiating `block`

[MartyO256]

Consider the following Twelf excerpt from the mechanization of Standard ML. Here, unmap-tequiv is proved in a world that includes unmap-bind:

%block unmap-bind
   : some {K:kind} {B:etp} {Dmap:tunmap B K} {Dwf:kd-wf K}
      block {a:con} {da:cn-of a K} {das:cn-assm da}
      {_:mcn-assm da das}
      {_:cn-of-reg da Dwf}
      {x:eterm} {dx:evof x B} {xt:unmap x a}
      {_:can-unmap x xt}
      {_:unmap-vof dx xt Dmap da}.

unmap-tequiv	: tequiv A B
		   -> tunmap A K
		   -> tunmap B L
%%
		   -> kd-equiv K L -> type.
%mode unmap-tequiv +X1 +X2 +X3 -X4.

-	: unmap-tequiv (tequiv/sigma DequivB DequivA) (tunmap/sigma DmapB1 DmapA1) (tunmap/sigma DmapB2 DmapA2)
	   (kd-equiv/sigma DequivB' DequivA')
	   <- unmap-tequiv DequivA DmapA1 DmapA2 DequivA'
	   <- kd-equiv-reg DequivA' DwfA' _
	   <- ({a} {e} {es}
		 mcn-assm e es
		 -> cn-of-reg e DwfA'
		 -> {x} {d} {xt}
		    can-unmap x xt
		 -> unmap-vof d xt DmapA1 e
		 -> unmap-tequiv (DequivB x d) (DmapB1 x a xt) (DmapB2 x a xt) (DequivB' a e)).

For the last appeal to the induction hypothesis, DwfA' (obtained by kd-equiv-reg DequivA' DwfA' _) is a proof that the kind of constructor a is well-formed. This is asserted by -> cn-of-reg e DwfA'.

DwfA' is required to instantiate the block in unmap-bind because we have some ... {Dwf:kd-wf K} block .... Otherwise the appeal to the induction hypothesis would fail because unmap-tequiv is not necessarily provable in the variable case with the weaker world that does not require {Dwf:kd-wf K}.

In Beluga/Harpoon, that appeal to the induction hypothesis works even though DwfA' is not proved. This may not be sound.

Below is a translation of the Twelf excerpt without using kd-equiv-reg:

LF con : type =;
LF kind : type =
| sigma : kind -> (con -> kind) -> kind
;

LF cn-of : con -> kind -> type =;
LF kd-wf : kind -> type =;

LF eterm : type =
and etp : type =
| esigma : etp -> (eterm -> etp) -> etp
;

LF unmap : eterm -> con -> type =;
LF tunmap : etp -> kind -> type =
| tunmap/sigma :
  tunmap A1 K1 ->
  ({x : eterm} {a : con} unmap x a ->
   tunmap (A2 x) (K2 a)) ->
    tunmap (esigma A1 A2) (sigma K1 K2)
;
--name tunmap Dtunmap.
LF eof : eterm -> etp -> type =;
LF tequiv : etp -> etp -> type =
| tequiv/sigma :
  tequiv A A' ->
  ({ x : eterm } eof x A -> tequiv (B x) (B' x)) ->
    tequiv (esigma A B) (esigma A' B')
;
--name tequiv Dtequiv.

LF kd-equiv : kind -> kind -> type =
| kd-equiv/sigma :
  kd-equiv K1 K1' ->
  ({ a : con } cn-of a K1 -> kd-equiv (K2 a) (K2' a)) ->
    kd-equiv (sigma K1 K2) (sigma K1' K2')
;

schema unmap-bind =
  some [K : kind, B : etp, Dmap : tunmap B K, Dwf : kd-wf K]
  block (a : con, da : cn-of a K, x : eterm, dx : eof x B, xt : unmap x a);

proof unmap-tequiv :
  (g : unmap-bind)
  [g |- tequiv A B] ->
  [g |- tunmap A K] ->
  [g |- tunmap B L] ->
    [g |- kd-equiv K L] =
/ total 1 /
intros
{ g : unmap-bind,
  A : (g |- etp),
  B : (g |- etp),
  K : (g |- kind),
  L : (g |- kind)
| x : [g |- tequiv A B], x1 : [g |- tunmap A K], x2 : [g |- tunmap B L]
; split x as
  case tequiv/sigma:
  { g : unmap-bind,
    X : (g |- etp),
    X2 : (g, x : eterm |- etp),
    X1 : (g |- etp),
    X3 : (g, z : eterm |- etp),
    K : (g |- kind),
    L : (g |- kind),
    Dtequiv : (g |- tequiv X X1),
    Dtequiv1 :
      (g, x : eterm, y : eof x (X[..]) |- tequiv (X2[.., x]) (X3[.., x]))
  | x : [g |- tequiv (esigma X (\z2. X2)) (esigma X1 (\z2. X3))],
    x1 : [g |- tunmap (esigma X (\z2. X2)) K],
    x2 : [g |- tunmap (esigma X1 (\z2. X3)) L]
  ; split x1 as
    case tunmap/sigma:
    { g : unmap-bind,
      X : (g |- etp),
      X2 : (g, x : eterm |- etp),
      X1 : (g |- etp),
      X3 : (g, z : eterm |- etp),
      X5 : (g |- kind),
      X7 : (g, z : con |- kind),
      L : (g |- kind),
      Dtequiv : (g |- tequiv X X1),
      Dtequiv1 :
        (g, x : eterm, y : eof x (X[..]) |- tequiv (X2[.., x]) (X3[.., x])),
      Dtunmap : (g |- tunmap X X5),
      Dtunmap1 :
        (g, x : eterm, a : con, y : unmap x a |-
           tunmap (X2[.., x]) (X7[.., a]))
    | x : [g |- tequiv (esigma X (\z2. X2)) (esigma X1 (\z2. X3))],
      x1 : [g |- tunmap (esigma X (\z2. X2)) (sigma X5 (\z. X7))],
      x2 : [g |- tunmap (esigma X1 (\z2. X3)) L]
    ; split x2 as
      case tunmap/sigma:
      { g : unmap-bind,
        X : (g |- etp),
        X2 : (g, x : eterm |- etp),
        X1 : (g |- etp),
        X3 : (g, z : eterm |- etp),
        X5 : (g |- kind),
        X7 : (g, z : con |- kind),
        X9 : (g |- kind),
        X11 : (g, z : con |- kind),
        Dtequiv : (g |- tequiv X X1),
        Dtequiv1 :
          (g, x : eterm, y : eof x (X[..]) |- tequiv (X2[.., x]) (X3[.., x])),
        Dtunmap : (g |- tunmap X X5),
        Dtunmap1 :
          (g, x : eterm, a : con, y : unmap x a |-
             tunmap (X2[.., x]) (X7[.., a])),
        Dtunmap2 : (g |- tunmap X1 X9),
        Dtunmap3 :
          (g, x : eterm, a : con, y : unmap x a |-
             tunmap (X3[.., x]) (X11[.., a]))
      | x : [g |- tequiv (esigma X (\z2. X2)) (esigma X1 (\z2. X3))],
        x1 : [g |- tunmap (esigma X (\z2. X2)) (sigma X5 (\z. X7))],
        x2 : [g |- tunmap (esigma X1 (\z2. X3)) (sigma X9 (\z. X11))]
      ; by unmap-tequiv [_ |- Dtequiv] [_ |- Dtunmap] [_ |- Dtunmap2]
        as D1 unboxed;
        by unmap-tequiv
             [_,
              b :
                block (
                  a : con,
                  da : cn-of a _,
                  x : eterm,
                  dx : eof x _,
                  xt : unmap x a) |- Dtequiv1[.., b.3, b.4]]
             [_,
              b :
                block (
                  a : con,
                  da : cn-of a _,
                  x : eterm,
                  dx : eof x _,
                  xt : unmap x a) |- Dtunmap1[.., b.3, b.1, b.5]]
             [_,
              b :
                block (
                  a : con,
                  da : cn-of a _,
                  x : eterm,
                  dx : eof x _,
                  xt : unmap x a) |- Dtunmap3[.., b.3, b.1, b.5]]
        as D2 strengthened;
        solve [g |- kd-equiv/sigma D1 (\a. \da. D2)]
      }
    }
  }
}
;