From 46b07e87e1d95880f89f158e3bd71c16119b9f7d Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 17 Jun 2020 13:52:03 +0200
Subject: [PATCH] not injective

---
 encodings/subtype_poly.lp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/encodings/subtype_poly.lp b/encodings/subtype_poly.lp
index 50c71ca..58e97a9 100644
--- a/encodings/subtype_poly.lp
+++ b/encodings/subtype_poly.lp
@@ -44,7 +44,7 @@ symbol cstr_maxcast_idem: ε (∀B (λt, ∀ {t} (λx, π t (maxcast x))))
 private constant symbol max_eq: Set → Set → Bool
 set infix 6 "≃" ≔ max_eq
 
-injective symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η fr → η to
+symbol eqcast {fr: Set} {to: Set}: ε (fr ≃ to) → η fr → η to
 
 definition compatible (t u: Set) ≔ μ t ≃ μ u
 set infix 6 "~" ≔ compatible
-- 
GitLab