Function same_proof_shape 

pub fn same_proof_shape(a: &Expr, b: &Expr) -> bool

Checks whether two proof terms have structurally identical shapes, ignoring the actual constants and literals at the leaves.