[ ... ] match t in t with ==> match t in t return ... with
\forall p:A \lor B. P p.
intros.
apply
\forall p:A \lor B. P p.
intros.
apply
- ([\lambda p.P p]
- match p with
+ (match p return \lambda p.P p with
[(or_introl p) \Rightarrow H p
|(or_intror q) \Rightarrow H1 q]).
qed.
[(or_introl p) \Rightarrow H p
|(or_intror q) \Rightarrow H1 q]).
qed.
P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
intros.
exact
P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
intros.
exact
- ([\lambda y. \lambda p.P y p]
- match p with
+ (match p return \lambda y. \lambda p.P y p with
[refl_eq \Rightarrow H]).
qed.
[refl_eq \Rightarrow H]).
qed.
simplify.assumption.
simplify.
apply (bool_ind (\lambda b:bool.
simplify.assumption.
simplify.
apply (bool_ind (\lambda b:bool.
-(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (S n1) = b) \to (f (match b in bool with
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true)).
simplify.intro.assumption.
[ true \Rightarrow (S n1)
| false \Rightarrow (max n1 f)])) = true)).
simplify.intro.assumption.
apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
simplify.
apply (bool_ind (\lambda b:bool.
apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
simplify.
apply (bool_ind (\lambda b:bool.
-(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (m-(S n)) = b) \to (f (match b in bool with
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true)).
simplify.intro.assumption.
[ true \Rightarrow m-(S n)
| false \Rightarrow (min_aux n m f)])) = true)).
simplify.intro.assumption.
<keyword>qed</keyword>
<keyword>rec</keyword>
<keyword>record</keyword>
<keyword>qed</keyword>
<keyword>rec</keyword>
<keyword>record</keyword>
+ <keyword>return</keyword>
<keyword>to</keyword>
<keyword>using</keyword>
<keyword>with</keyword>
<keyword>to</keyword>
<keyword>using</keyword>
<keyword>with</keyword>