Open jprider63 opened 4 years ago
Integrate with Yiyun's branch of LH and move the proofs into typeclass instances.
Integrate with Yiyun's branch of LH and move the proofs into typeclass instances.