proposition: Lemma AR_strengthen (p1 q1 p2 q2 : X -> Prop) w : (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) -> cAR p1 q1 w -> cAR p2 q2 w.
proof: Proof. move => H1 H2. move: w. cofix AR_strengthen => w. case => [ /H1 ? /H2 ?|/H2 ? N]; first exact: AR0. apply: ARs => // v wv. apply: AR_strengthen. exact: N. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)