∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
#R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1