iris_check.v now imports derived_rules

iris_check.v

 Require Import Arith ssreflect.
-Require Import world_prop world_prop_recdom core_lang lang masks iris_core iris_plog iris_meta iris_vs_rules iris_ht_rules.
+Require Import world_prop world_prop_recdom core_lang lang masks iris_core iris_plog iris_meta iris_vs_rules iris_ht_rules iris_derived_rules.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
@@ -182,6 +182,7 @@ Module Import Plog := IrisPlog TrivialRA StupidLang Res World Core.
 Module Import Meta := IrisMeta TrivialRA StupidLang Res World Core Plog.
 Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
 Module Import VSRules := IrisVSRules TrivialRA StupidLang Res World Core Plog.
+Module Import DRRules := IrisDerivedRules TrivialRA StupidLang Res World Core Plog VSRules HTRules.
 
 (* And now we check for axioms *)
 Print Assumptions adequacy_obs.