Implicit Arguments On.
Lemma loop_variant_1 :
(A:Set)(v,phi0:A)(I:Prop)(P:A->Prop)
v=phi0 -> (I /\ (P phi0)) -> (P v).
Proof.
Intros. Rewrite H. Tauto.
Save.
Lemma why_rewrite_var :
(A:Set)(x,t:A)x=t->(P:A->Prop)(P x)->(P t).
Proof.
Intros; Case H; Trivial.
Save.
Implicits why_rewrite_var [1 2 3].
Lemma why_boolean_case :
(A,B,C,D:Prop)
(b:bool)(if b then A else B)->(A->C)->(B->D)->(if b then C else D).
Proof.
Destruct b; Intuition.
Save.