diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-08 00:52:52 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-08 00:52:52 -0500 |
commit | 960c26fe3c931b555e69240c639eaed8c378dd4b (patch) | |
tree | 92a1d53bc7a1c32457e5d470d3261528fa54201b | |
parent | 978ecdd839bfcdcfc4b086c5fbd6d68515e5334c (diff) |
add wf_smart_Literal_eq
-rw-r--r-- | src/LanguageWf.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/LanguageWf.v b/src/LanguageWf.v index da5db2944..0e4822701 100644 --- a/src/LanguageWf.v +++ b/src/LanguageWf.v @@ -1078,6 +1078,11 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [ | progress rewrite in_map_iff in * | solve [ auto ] ]. Qed. + + Lemma wf_smart_Literal_eq {t v1 v2 G} + : v1 = v2 -> expr.wf G (@ident.smart_Literal var1 t v1) (@ident.smart_Literal var2 t v2). + Proof using Type. intro; subst; apply wf_smart_Literal. Qed. + Qed. End with_var2. Lemma Wf_Reify_as {t} v : expr.Wf (@GallinaReify.base.Reify_as t v). |