(* Basic inversion properties ***********************************************)
lemma max_inv_dx: βri,rs,ti,ts,c1,c2. β©ri,rs,ti,tsβͺ = (c1 β¨ c2) β
(* Basic inversion properties ***********************************************)
lemma max_inv_dx: βri,rs,ti,ts,c1,c2. β©ri,rs,ti,tsβͺ = (c1 β¨ c2) β