proposition: Lemma L4 : forall b i j, reachable (quad (f b) i (S j) 0) -> reachable (quad (f (S b)) i j 0).
proof: Proof. intros. econstructor 3. unfold reachable in H. eexact H. rewrite f_Sn. apply L3. Qed.
imports: Arith Omega Relations