Fix potential for cycles in trust substitutions (#7687)

Fix potential for cycles in trust substitutions (#7687)

This ensures we use only the prefix of substitutions for the *first* time a formula is proven in a substitution map.

This avoids the possibility for cycles in proof generators during non-clausal simplification, where we may reprove a formula F later at a point where later substitutions depend on F.