A Constraint Language for Static Semantic Analysis Based on Scope Graphs with Proofs