proposition: Lemma eqitC_wcompat b1 b2 vclo (MON: monotone2 vclo) (CMP: compose (eqitC b1 b2) vclo <3= compose vclo (eqitC b1 b2)): wcompatible2 (@eqit_ E R1 R2 RR b1 b2 vclo) (eqitC b1 b2).
proof: Proof. Proof with eauto with paco itree. econstructor; [ eauto with paco itree | ]. intros. destruct PR. punfold EQVl. punfold EQVr. unfold_eqit. hinduction REL before r; intros; clear t1' t2'. - remember (RetF r1) as x. hinduction EQVl before r; intros; subst; try inv Heqx; [ | eauto with itree ]. remember (RetF r3) as y. hinduction EQVr before r; intros; subst; try inv Heqy... - remember (TauF m1) as x. hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; [ | eauto with itree ]. remember (TauF m3) as y. hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; [ | eauto with itree ]. pclearbot. econstructor. gclo. econstructor; eauto with paco. - remember (VisF e k1) as x. hinduction EQVl before r; intros; try discriminate Heqx; [ inv_Vis | eauto with itree ]. remember (VisF e k3) as y. hinduction EQVr before r; intros; try discriminate Heqy; [ inv_Vis | eauto with itree ]. econstructor. intros. pclearbot. eapply MON. + apply CMP. econstructor... + intros. apply gpaco2_clo, PR. - remember (TauF t1) as x. hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; [ | eauto with itree ]. pclearbot. punfold REL... - remember (TauF t2) as y. hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; [ | eauto with itree ]. pclearbot. punfold REL... Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)