proposition: Lemma product_fixpoint : forall m1 m2, itree_similar (product m1 m2) (Product product m1 m2).
proof: Proof. Proof using. apply (FixFun2Mod_corec itree_family). reflexivity. apply itree_similar_eq. apply itree_family_COFE. simpl. introv H. destruct i. simple~. unfold Product. destruct x1; destruct x2; simpl; auto with maths. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat