add crude support for flattening with LetRec and Case at level zero

[coq-hetmet.git] / src / ReificationCategory.v

diff --git a/src/ReificationCategory.v b/src/ReificationCategory.v
index 9a7c3fd..2261f88 100644 (file)
--- a/src/ReificationCategory.v
+++ b/src/ReificationCategory.v
@@ -97,6 +97,7 @@ Definition compose_reifications (s0 s1 s2:SMMEs) :
   apply (ni_respects2 (a >>>> a') (b >>>> b') x).
   apply ni_inv.
   apply comm1.
+  apply (reification_host_lang_pure _ _ _ X0).
   Defined.
 
 Definition reificationOrIdentityComp