Function lemma_disjoint_refs 

pub proof fn lemma_disjoint_refs<Left: SpecParser, Right: SpecParser>(
    left: Ref<Left>,
    right: Ref<Right>,
)

requires

disjoint_domains(left.0, right.0),

ensures

#[trigger] disjoint_domains(left, right),

Compatibility helper for two borrowing adapters.

This fact is kept directly callable but is not broadcast; the directional Ref rules derive it without adding another competing trigger path.