For sake of readability, we only describe simplified rules covering all cases.
  
p : αpq: τq; 1⟩ = ⟨p : τpr : τr; 1⟩ = e
p : αpq : τq; r : τr; 1⟩ = e ∧ αp = τp
  
p : τp; 1⟩ = ⟨p : αpq : τq; 0⟩ = e
p : τpq : τq; 0⟩ = e ∧ αp = τp
  
p : τp; 0⟩ = ⟨p : αp; 0⟩ = e
p : αp; 0⟩ = e ∧ αp = τp
        
  
q : τq; 0⟩ = ⟨r : τr; 0⟩ = e
The generalization is obvious: the occurrences of pp, pp, qq, and rr, can be replaced by finite mappings from labels to types P, P', Q, and R of disjoint domain except for P and P' of identical domain.

These (generalized) rules should be added to those for simple types, where rule Fail and Decompose are not extended to the object type constructor, nor the row constructors.