pair-eta/README.md


			
				
				
					
						
						
						
							
							
							This repository contains a proof of pi injectivity for an untyped equational theory with surjective pairing and extensionality.

						
						
					
				
				
					
						Reference in a new issue
					
					View git blame
					Copy permalink