add wf_smart_Literal_eq

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).