Definition RV (k : nat) (T : Ty) (rho : tymapping) (v v' : Term) : Prop :=
value v /\ value v' /\ RC k T rho v v'.
And we have a "converting" lemma:
Lemma RV_RC k T rho e e' :
RC k T rho e e' <->
(forall j (Hlt_j : j < k) e_f,
e =[j]=> e_f ->
exists e'_f j', e' =[j']=> e'_f /\ RV (k - j) T rho e_f e'_f
).
This means that:
A lot of places that use RV will have to be updated, unclear in what way
Use mutual recursion with non-structural induction on the step index k (i < k). So preferably use equation again, does it support mutual recursion?
Now,
RV
is a bit of a hack:And we have a "converting" lemma:
This means that:
RV
will have to be updated, unclear in what way