proposition: Lemma demo_splits : test_split_3.
proof: Proof. Proof using. dup 4. split. demo. split. demo. split. demo. split. demo. demo. splits 4. demo. demo. demo. demo. splits 3. demo. demo. demo. splits. demo. demo. demo. splits. demo. demo. demo. Qed.
imports: TLC(LibTactics) Coq.micromega.Lia