search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Useful lemma #65

Closed jldodds closed 9 years ago

jldodds commented 9 years ago

I've found the following nice, and I don't think it is in mirror-core yet:

Lemma exprD'_one_type : forall tus tvs t1 t2 (e : expr typ func) v1 v2,
exprD' tus tvs t1 e = Some v1 ->
exprD' tus tvs t2 e = Some v2 ->
t1 = t2.
Proof.
intros.
apply ExprTac.exprD_typeof_Some in H; try apply _.
eapply ExprTac.exprD_typeof_eq in H0. symmetry.
eauto. apply _. apply _. apply _. auto.
Qed.
gmalecha commented 9 years ago

This is in there. exprD'_single_type