added proofs by case analysis
added some support for local assumptions