proposition: Fact subrel_and2 X Y (R1 R2 R3 R4 : Rel X Y) : R1 <<=2 R3 /\ R2 <<=2 R4 -> R1 ∩ R2 <<=2 R3 ∩ R4.
proof: Proof. firstorder. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Undecidability.Shared.Libs.PSL.Vectors.Vectors