rw [composeBinary, PropagateStruc.eval_compose, q₁.good, q₂.good]
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
⊢ PropagateStruc.eval (composeBinary p q₁ q₂) x =
    PropagateStruc.eval p fun b =>
      bif b then evalFin t₁ fun i => x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
      else evalFin t₂ fun i => x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
α β α' β' : Type
γ : β → Type
p : PropagateStruc Bool
t₁ t₂ : Term
q₁ : PropagateSolution t₁
q₂ : PropagateSolution t₂
x : Fin (max (arity t₁) (arity t₂)) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a =>
      PropagateStruc.eval
        (match a with
        | true => q₁.toPropagateStruc
        | false => q₂.toPropagateStruc)
        fun i =>
        x (↑(Fin.castLe (_ : (bif a then arity t₁ else arity t₂) ≤ max (arity t₁) (arity t₂))).toEmbedding i)) =
    PropagateStruc.eval p fun b =>
      bif b then
        PropagateStruc.eval q₁.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₁ ≤ max (arity t₁) (arity t₂))).toEmbedding i)
      else
        PropagateStruc.eval q₂.toPropagateStruc fun i =>
          x (↑(Fin.castLe (_ : arity t₂ ≤ max (arity t₁) (arity t₂))).toEmbedding i)