Open jaccokrijnen opened 1 year ago
This will also impact the definition of RG
:
(** RG = Interpretation of type contexts as logically related term environments *)
Inductive RG (rho : tymapping) (k : nat) : tass -> env -> env -> Prop :=
| RG_nil :
RG rho k nil nil nil
| RG_cons : forall x T v1 v2 c e1 e2,
RV k T rho v1 v2 ->
normal_Ty T ->
RG rho k c e1 e2 ->
RG rho k ((x, T) :: c) ((x, v1) :: e1) ((x, v2) :: e2).
The dead-code proof needs to construct related gamma substitutions, in the case of strict
we know from the big-step rule that the bound term terminates with a value, and use that to construct related gamma substitutions. In this case we don't know that, but we still want to construct related substitutions. Would it be enough to change the RV argument to RC? What would break?
Currently: