-letin program ≝
- (λl:list nat. λH:l ≠ [].match l with [ nil ⇒ λH.[] | cons x l1 ⇒ λH.l1] H);
-letin program_spec ≝ (program : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l);
- [ generalize in match H; cases l; [intros (h1); cases (h1 ?); reflexivity]
- intros; apply (ex_intro ? ? n); apply eq_f; reflexivity; ]
-exact program_spec;
+ apply rule (λl:list nat. λ_.match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
+ [ exists; [2: reflexivity | skip]
+ | destruct; elim H; reflexivity]