[TYPES] Replacement lemma

[Sunil Kothari]

Hello All,
   I sent the below query to Coq mailing list but generated no response. My apologies if you receive multiple copies of this email. 
I was wondering if there are any machine checked proofs (in any theorem prover) of replacement lemma [1,2] . I reproduce the lemma as stated by Wright and Felleisen in [1] below:
If
1. D is a derivation concluding  \Gamma |-  C [t]: \tau,
2. D1 is a sub-derivation of D concluding \Gamma’ |- t :\tau',
3. D1 occurs in D in the position corresponding to the hole ([]) in C, and
4. \Gamma' |- t’ : \tau' is derivable.
Then  \Gamma |- C[t’] :\tau is derivable .

Also, I wanted to know if there is a corresponding lemma in a constraint setting where the sequent becomes a 4-place relation. For example, \Gamma, E |- t: \tau, where E denotes a list of equational constraints.  If there is such a lemma, has it been formalized in any theorem prover ?

Any pointers/references will be highly appreciated.

Thanks,
Sunil



References:
[1] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type
soundness. Information and Computation, 115(1):38-94, 1994.
[2] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators
and /\-Calculus. Cambridge University Press, 1986.