lemma a_equal_b:
  assumes 1:"vec n a" and  2:"vec n b" and 3:"vec n l" and 4:"∀i∈set [0..<n]. vec n (m!i)"  and 5:"∀i∈set [0..<n]. ewp_vec (m!i)" and
    6:"∀i∈set [0..<n].   equations a (m!i) + l!i = a!i"  and
    7:"∀i∈set [0..<n].   equations b (m!i) + l!i = b!i"
  shows "∀i∈set [0..<n]. a!i = b!i" using assms
proof (induct n)
  case 0
  then show ?case using assms by simp
next
  case (Suc n)
  then show ?case
  proof (induct n)
    case 0
    then show ?case apply auto
      by (smt (verit, del_insts) "0.prems"(5) "0.prems"(6) "1" "6" "7" One_nat_def base_case vec_def)
  next
    case (Suc n)
    then show ?case
    proof -
      assume i1:"vec (Suc (Suc n)) a" and i2:"vec (Suc (Suc n)) b" and i3:"vec (Suc (Suc n)) l" and
        i4:"∀i∈set [0..<Suc (Suc n)]. vec (Suc (Suc n)) (m ! i)" and
        i5:"∀i∈set [0..<Suc (Suc n)]. ewp_vec (m ! i)" and
        i6:"∀i∈set [0..<Suc (Suc n)]. equations a (m ! i) + l ! i = a ! i" and
        i7: "∀i∈set [0..<Suc (Suc n)]. equations b (m ! i) + l ! i = b ! i"
      have co6:"∀i∈set [0..<(Suc n)].  a!i = equations (butlast a) (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))  +
          l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i" using i1 i3 i4 i6 i5 m12[of "Suc n" a l m] by blast
      from co6 i1 have cof1:"∀i∈set [0..<(Suc n)].  equations (butlast a) (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))  +
          l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i = (butlast a)!i "
        by (simp add: nth_butlast vec_def)

      have c07:"∀i∈set [0..<(Suc n)].  b!i = equations (butlast b) (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))  +
          l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i" using i2 i3 i4 i7 i5 m12[of "Suc n" b l m] by blast
      from c07 i2 have cof2:"∀i∈set [0..<(Suc n)].  equations (butlast b) (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))  +
          l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i = (butlast b)!i"
        by (simp add: nth_butlast vec_def)

      have co1: "vec (Suc n) (butlast a)" using i1 by(simp add:vec_def)
      have co2: "vec (Suc n) (butlast b)" using i2 by(simp add:vec_def)
      have co3: "∀i∈set [0..<Suc n]. vec (Suc n) (map (λi. l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i) [0..<Suc n])" using i4 sorry
      have co4: "∀i∈set [0..<Suc n]. ewp_vec (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))" using i5 sorry
      have c1: "∀i∈set [0..<(Suc n)]. a ! i = b ! i" using co1 co2 co3 co4 cof1 cof2 Suc.hyps sledgehammer
        using co6 by fastforce
      moreover have "a !(Suc n) = b ! (Suc n)" using i1 i2 i3 i4 i5 i6 i7 proof -
        have cc1:"a!(Suc n) = (equations (butlast a) (butlast (m!(Suc n))) + l!(Suc n)) * (m!(Suc n)!(Suc n))⇧⋆"
          using i1 i3 i4 i5 i6 m5 by blast
        moreover have cc2: "b!(Suc n) = (equations (butlast b) (butlast (m!(Suc n))) + l!(Suc n)) * (m!(Suc n)!(Suc n))⇧⋆"
          using i2 i3 i4 i5 i7 m5 by blast
        moreover have "(butlast a) = (butlast b)" using c1 i1 i2 apply (simp add:vec_def)
        proof -
          have "take (length a - 1) a  = take (length b - 1) b"  using c1 i1 i2 apply (simp add:vec_def)
            using aux_2 by blast
          then show ?thesis
            by (metis take_replace)
        qed
         ultimately show ?thesis
          by presburger
      qed
      ultimately show ?thesis
        by simp
    qed
  qed
qed

 vec (Suc n) a ⟹
    vec (Suc n) b ⟹
    vec (Suc n) l ⟹
    ∀i∈set [0..<Suc n]. vec (Suc n) (m ! i) ⟹
    ∀i∈set [0..<Suc n]. ewp_vec (m ! i) ⟹
    ∀i∈set [0..<Suc n]. equations a (m ! i) + l ! i = a ! i ⟹ ∀i∈set [0..<Suc n]. equations b (m ! i) + l ! i = b ! i ⟹ ∀i∈set [0..<Suc n]. a ! i = b ! i

 have co1: "vec (Suc n) (butlast a)" using i1 by(simp add:vec_def)
      have co2: "vec (Suc n) (butlast b)" using i2 by(simp add:vec_def)
      have co3: "∀i∈set [0..<Suc n]. vec (Suc n) (map (λi. l!(Suc n) * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n)) + l!i) [0..<Suc n])" using i4 sorry
      have co4: "∀i∈set [0..<Suc n]. ewp_vec (map2 (+) (butlast (m!i)) (map (λr. r * (m!(Suc n)!(Suc n))⇧⋆ * (m!i!(Suc n))) (butlast (m!(Suc n)))))" using i5 sorry
      have c1: "∀i∈set [0..<(Suc n)]. a ! i = b ! i" using co1 co2 co3 co4 cof1 cof2 Suc.hyps sorry