diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-09-21 20:45:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-09-22 10:44:07 -0400 |
| commit | 5357fe92e65712a3e2506fe0a939b358d14183d7 (patch) | |
| tree | ea0328c53e10620d9a46cd13606a5b6646ce7d6f /src/Util/LetIn.v | |
| parent | fd5cba50d8743149e7ca4e386716126f2fc03e63 (diff) | |
alternative signing derivation
cleanup
Diffstat (limited to 'src/Util/LetIn.v')
| -rw-r--r-- | src/Util/LetIn.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v index a472f4090..80310b833 100644 --- a/src/Util/LetIn.v +++ b/src/Util/LetIn.v @@ -14,9 +14,11 @@ Global Instance Proper_Let_In_nd_changevalue {A B} (RA:relation A) {RB:relation : Proper (RA ==> (RA ==> RB) ==> RB) (Let_In (P:=fun _=>B)). Proof. cbv; intuition. Qed. -Lemma app_Let_In_nd {A B C} (f:B -> C) : forall (e:A) (C:A -> B), - f (Let_In e C) = Let_In e (fun v => f (C v)). -Proof. cbv; intuition. Qed. +Definition app_Let_In_nd {A B T} (f:B->T) (e:A) (C:A->B) + : f (Let_In e C) = Let_In e (fun v => f (C v)) := eq_refl. + +Definition Let_app_In_nd {A B T} (f:A->B) (e:A) (C:B->T) + : Let_In (f e) C = Let_In e (fun v => C (f v)) := eq_refl. Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T. (* : forall T, gallina T -> gallina T, structurally recursive in the argument *) |