rfl
α β α' β' : Type
γ : β → Type
p : PropagateStruc Unit
t : Term
q : PropagateSolution t
x : Fin (arity t) → ℕ → Bool
⊢ (PropagateStruc.eval p fun a => PropagateStruc.eval q.toPropagateStruc fun i => x (id i)) =
    PropagateStruc.eval p fun x_1 => PropagateStruc.eval q.toPropagateStruc x
no goals