proposition: Lemma euttge_trans_clo_wcompat E1 E2 R1 R2 (REv : forall A B, E1 A -> E2 B -> Prop) (RAns : forall A B, E1 A -> A -> E2 B -> B -> Prop ) (RR : R1 -> R2 -> Prop) : wcompatible2 (rutt_ REv RAns RR) (euttge_trans_clo RR).
proof: Proof. constructor; eauto with paco. { red. intros. eapply euttge_trans_clo_mon; eauto. } intros. destruct PR. punfold EQVl. punfold EQVr. unfold_eqit. hinduction REL before r; intros; clear t1' t2'. - remember (RetF r1) as x. red. hinduction EQVl before r; intros; subst; try inv Heqx; eauto; (try constructor; eauto). remember (RetF r3) as x. hinduction EQVr before r; intros; subst; try inv Heqx; (try constructor; eauto). - red. remember (TauF m1) as x. hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; ( try (constructor; eauto; fail )). remember (TauF m3) as y. hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; (try (constructor; eauto; fail)). pclearbot. constructor. gclo. econstructor; eauto with paco. - remember (VisF e1 k1) as x. red. hinduction EQVl before r; intros; subst; try discriminate; try (constructor; eauto; fail). remember (VisF e2 k3) as y. hinduction EQVr before r; intros; subst; try discriminate; try (constructor; eauto; fail). dependent destruction Heqx. dependent destruction Heqy. constructor; auto. intros. apply H0 in H1. pclearbot. apply gpaco2_clo. econstructor; eauto with itree. - remember (TauF t1) as x. red. hinduction EQVl before r; intros; subst; try inv Heqx; try inv CHECK; (try (constructor; eauto; fail)). pclearbot. punfold REL. constructor. eapply IHREL; eauto. - remember (TauF t2) as y. red. hinduction EQVr before r; intros; subst; try inv Heqy; try inv CHECK; (try (constructor; eauto; fail)). pclearbot. punfold REL. constructor. eapply IHREL; eauto. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)