asl zarb

Goal (|{l | |l| = 4 ∧ (∀ x, x in l -> 0 ≤ x  ∧ x < 10) ∧ ~ head 0 l = 0 }| = 9 * 10 * 10 * 10);
Proof;
replace #1 ({ l: list ℤ | |l| = 4 ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ head 0 l = 0 }) with ({ l: list ℤ | ∃ a b c d: ℤ,  l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0 });
apply set_from_func_eq;
intros;
apply and_intro;
intros;
destruct H with (ex_ind ? ?) to (a a_property);
destruct a_property with (ex_ind ? ?) to (b b_property);
destruct b_property with (ex_ind ? ?) to (c c_property);
destruct c_property with (ex_ind ? ?) to (d d_property);
destruct d_property with (and_ind ? ?) to (d_property_l d_property_r);
z3;
intros;
apply (ex_intro ? ? (nth 0 x 0));
apply (ex_intro ? ? (nth 0 x 1));
apply (ex_intro ? ? (nth 0 x 2));
apply (ex_intro ? ? (nth 0 x 3));
z3;
apply eq_sym ;
replace #1 (9 * 10 * 10 * 10) with (10 * 10 * 10 * 9);
lia;
apply eq_sym ;
apply (⁨asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ a: ℤ,
  λ l: list ℤ,
    ∃ b c d: ℤ,
      l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ x: ℤ,
  0 < x ∧ x < 10) ?24 ?26 ?28 ?30⁩);
intros;
destruct H with (ex_ind ? ?) to (l l_property);
destruct l_property with (ex_ind ? ?) to (l_property_value l_property_proof) ;
destruct l_property_proof with (ex_ind ? ?) to (l_property_proof_value l_property_proof_proof) ;
destruct l_property_proof_proof with (ex_ind ? ?) to (l_property_proof_proof_value l_property_proof_proof_proof) ;
destruct l_property_proof_proof_proof with (and_ind ? ?) to (l_property_proof_proof_proof_l l_property_proof_proof_proof_r) ;
destruct l_property_proof_proof_proof_r with (and_ind ? ?) to (l_property_proof_proof_proof_r_l l_property_proof_proof_proof_r_r) ;
add_hyp l_property_proof_proof_proof_r_l_ex := (l_property_proof_proof_proof_r_l (a));
z3;
intros;
destruct H0 with (ex_ind ? ?) to (H0_value H0_proof) ;
destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ;
destruct H0_proof with (ex_ind ? ?) to (H0_proof_value H0_proof_proof) ;
destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ;
destruct H0_proof_proof with (ex_ind ? ?) to (H0_proof_proof_value H0_proof_proof_proof) ;
destruct H1_proof_proof with (ex_ind ? ?) to (H1_proof_proof_value H1_proof_proof_proof) ;
z3;
intros;
apply (⁨asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ b: ℤ,
  λ l: list ℤ,
    ∃ c d: ℤ,
      l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ b: ℤ,
  0 ≤ b ∧ b < 10) ?24 ?26 ?28 ?30⁩);
intros;
destruct H0 with (ex_ind ? ?) to (H0_value H0_proof) ;
destruct H0_proof with (ex_ind ? ?) to (H0_proof_value H0_proof_proof) ;
destruct H0_proof_proof with (ex_ind ? ?) to (H0_proof_proof_value H0_proof_proof_proof) ;
destruct H0_proof_proof_proof with (and_ind ? ?) to (H0_proof_proof_proof_l H0_proof_proof_proof_r) ;
destruct H0_proof_proof_proof_r with (and_ind ? ?) to (H0_proof_proof_proof_r_l H0_proof_proof_proof_r_r) ;
add_hyp H0_proof_proof_proof_r_l_ex := (H0_proof_proof_proof_r_l (a0));
z3;
intros;
destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ;
destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ;
destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ;
destruct H2_proof with (ex_ind ? ?) to (H2_proof_value H2_proof_proof) ;
z3;
intros b;
intros;
apply (⁨asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ c: ℤ,
  λ l: list ℤ,
    ∃ d: ℤ,
      l = [a, b, c, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ c: ℤ,
  0 ≤ c ∧ c < 10) ?24 ?26 ?28 ?30⁩);
intros;
destruct H1 with (ex_ind ? ?) to (H1_value H1_proof) ;
destruct H1_proof with (ex_ind ? ?) to (H1_proof_value H1_proof_proof) ;
destruct H1_proof_proof with (and_ind ? ?) to (H1_proof_proof_l H1_proof_proof_r) ;
destruct H1_proof_proof_r with (and_ind ? ?) to (H1_proof_proof_r_l H1_proof_proof_r_r) ;
add_hyp H1_proof_proof_r_l_ex := (H1_proof_proof_r_l (a0));
z3;
intros;
destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ;
destruct H3 with (ex_ind ? ?) to (H3_value H3_proof) ;
z3;
intros;
apply eq_sym ;
replace #1 (10) with (1 * 10);
lia;
apply eq_sym ;
apply (⁨asl_zarb3 ?0 ?2 ?4 ?6 ?8 (λ d: ℤ,
  λ l: list ℤ,
    l = [a, b, a0, d] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0) (λ d: ℤ,
  0 ≤ d ∧ d < 10) ?24 ?26 ?28 ?30⁩);
intros;
destruct H2 with (ex_ind ? ?) to (H2_value H2_proof) ;
destruct H2_proof with (and_ind ? ?) to (H2_proof_l H2_proof_r) ;
destruct H2_proof_r with (and_ind ? ?) to (H2_proof_r_l H2_proof_r_r) ;
add_hyp H2_proof_r_l_ex := (H2_proof_r_l (a1));
z3;
intros;
z3;
intros;
replace #1 ({ l: list ℤ | l = [a, b, a0, a1] ∧ (∀ x: ℤ, x in l → 0 ≤ x ∧ x < 10) ∧ ~ a = 0 }) with ({ [a, b, a0, a1]});
apply set_equality ;
apply included_fold ;
intros;
apply set_from_func_fold ;
apply and_intro ;
apply and_intro ;
lia;
intros;
z3;
auto_set;
apply included_fold ;
intros;
apply set_from_func_unfold in H3 ;
auto_set;
apply singleton_len ;