match p with
| add (.mk x) (.mk y) n =>
  apply ofLen_stmt_complete
  apply Or.inl; rfl
| sub (.mk x) (.mk y) m =>
  apply ofLen_stmt_complete
  apply Or.inr; rfl
| loop (.mk x) p =>
  dsimp [len]
  cases' x with x'
  match h: p.len with
  | 0 => exact False.elim $ Nat.ne_of_gt p.len_gt_zero h
  | 1 =>
    dsimp [ofLen, baseProgram]
    apply Finset.mem_union_right
    apply Finset.mem_image_of_mem
    exact lenOne_complete _ h
  | n + 1 =>
    apply ofLen_contains_extendLenOne_image
    rw [<- Nat.succ_eq_add_one, <- h]
    apply ofLen_complete
    cases p <;> simp [extendLenOne]
  apply ofLen_contains_extendLenOne_image
  case p => exact loop (.mk x') p
  have : p.len + x'.succ = (loop (.mk x') p).len := by rfl
  rw [this]
  apply ofLen_complete
  simp [extendLenOne]
| concat a b =>
  simp [len, ofLen]
  refine' .inr $ .inl (Finset.mem_fold_union_iff.mpr ⟨⟨a.len, _⟩, _⟩)
  rw [Finset.mem_range]; simp [len_gt_zero]
  simp; apply Finset.mem_product.mpr
  exact ⟨ofLen_complete _, ofLen_complete _⟩
p : LoopProgram
⊢ p ∈ ofLen (len p)
no goals