Commit 4c4a4777 authored by charguer's avatar charguer


parent 475146e9
......@@ -194,11 +194,28 @@ Proof using.
specializes C x. simpl pred. apply C.
Lemma App_partial : forall xs n f,
Lemma App_partial : forall n xs f,
curried n f -> (0 < length xs < n)%nat ->
App f xs \[] (fun g => \[ forall ys B H (Q:B->hprop),
App f (xs++ys) H Q -> App g ys H Q]).
Proof using.
(* TODO.
induction n. math. introv C N.
destruct xs as [|[A x] xs']. rew_list in N. math.
destruct n as [|n]. math.
lets: C x.
destruct xs' as [|[A' x'] xs''].
simpl. applys_eq H 1. apply func_ext_1.
intros g. fequal.
rew_list in N. math.
(* TODO...
induction xs; introv C E. rew_list in E. math.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment