proposition: Lemma ALRangeRelApp : forall R subl1 subl2 subr1 subr2, (ALRangeRel R subl1 subl2 # ALRangeRel R subr1 subr2) -> ALRangeRel R (subl1 ++ subr1) (subl2 ++ subr2).
proof: Proof. induction subl1 as [|(v1,t1) subl1 Hind]; introv Hsr; destruct subl2 as [|(v2,t2) subl2]; inverts Hsr; allsimpl;sp. Qed.
imports: list Omega